mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Basic
/-- Returns the first non-`none` result of applying `f` to each element of the array in reverse order,
from right to left. Returns `none` if `f` returns `none` for all elements of the array.

Examples:
 * `#[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
 * `#[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
Array.findSomeRev? : {α : Type u} → {β : Type v} → (α → Option β) → Array α → Option β
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F],
  F.PreservesZeroMorphisms
-- Mathlib.Data.Seq.Computation
Computation.thinkN_mem : ∀ {α : Type u} {s : Computation α} {a : α} (n : ℕ), a ∈ s.thinkN n ↔ a ∈ s
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a tuple does not change under scaling.  -/
Height.logHeight_smul_eq_logHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) {c : K},
  c ≠ 0 → Height.logHeight (c • x) = Height.logHeight x
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_eq_of_eq_add : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit b → a = c + b → a - b = c
-- Std.Do.PredTrans
Std.Do.PredTrans.mk.injEq : ∀ {ps : Std.Do.PostShape} {α : Type u} (trans : Std.Do.PostCond α ps → Std.Do.Assertion ps)
  (conjunctiveRaw : Std.Do.PredTrans.Conjunctive trans) (trans_1 : Std.Do.PostCond α ps → Std.Do.Assertion ps)
  (conjunctiveRaw_1 : Std.Do.PredTrans.Conjunctive trans_1),
  ({ trans := trans, conjunctiveRaw := conjunctiveRaw } = { trans := trans_1, conjunctiveRaw := conjunctiveRaw_1 }) =
    (trans = trans_1)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_one_adj : ∀ {u v : Fin 1}, ¬(SimpleGraph.cycleGraph 1).Adj u v
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X : C}
  {comon : CategoryTheory.ComonObj X} {X_1 : C} {comon_1 : CategoryTheory.ComonObj X_1},
  { X := X, comon := comon } = { X := X_1, comon := comon_1 } → X = X_1 ∧ comon ≍ comon_1
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instIsMultiplicativeSchemeQuasiSeparated : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.QuasiSeparated
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f g : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (a : α), f a ^ p ∂μ < ⊤ → ∫⁻ (a : α), g a ^ p ∂μ < ⊤ → 1 ≤ p → ∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_univ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.Substructure.closure L).toFun Set.univ = ⊤
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_symmDiff_le : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (u : Set α),
  autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_symmDiff_le._auto_1 →
    autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_symmDiff_le._auto_3 →
      μ.real (symmDiff s u) ≤ μ.real (symmDiff s t) + μ.real (symmDiff t u)
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_set_bind : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (s s' : σ) (mx : m α),
  (do
      set s
      set s'
      mx) =
    do
    set s'
    mx
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (x : N),
  (AddMonoid.Coprod.swap M N) (AddMonoid.Coprod.inr x) = AddMonoid.Coprod.inl x
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.getImpl.match_1.splitter : {α : Type u_1} →
  (motive : Lean.RArray α → Sort u_2) →
    (a : Lean.RArray α) →
      ((x : α) → motive (Lean.RArray.leaf x)) →
        ((p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)) → motive a
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_smul_apply : ∀ {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module S V] [inst_5 : AddCommMonoid W]
  [inst_6 : Module R W] [inst_7 : Module S W] [inst_8 : SMulCommClass R S W] [inst_9 : SMul S R]
  [inst_10 : IsScalarTower S R V] [inst_11 : IsScalarTower S R W] (e : V ≃ₗ[R] W) (α : Sˣ) (x : W),
  (α • e).symm x = ↑α⁻¹ • e.symm x
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.literal.injEq : ∀ {α : Type} (a a_1 : α),
  (Std.Tactic.BVDecide.BoolExpr.literal a = Std.Tactic.BVDecide.BoolExpr.literal a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.instMonoPushoutInr : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.meas_eLpNormEssSup_lt : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : ENorm ε] {f : α → ε},
  μ {y | MeasureTheory.eLpNormEssSup f μ < ‖f y‖ₑ} = 0
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subRight_symm : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G),
  (IsometryEquiv.subRight c).symm = IsometryEquiv.addRight c
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformContinuous_singleton : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous fun x => {x}
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` is strictly monotone on a left neighborhood of `a` and the image of this
neighborhood under `f` includes `Iio (f a)`, then `f` is continuous at `a` from the left.  -/
StrictMonoOn.continuousWithinAt_left_of_surjOn : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  StrictMonoOn f s → s ∈ nhdsWithin a (Set.Iic a) → Set.SurjOn f s (Set.Iio (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.Data.Matrix.Basis
Matrix.single_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : NonUnitalNonAssocSemiring α] [inst_3 : Fintype m] (i : n) (j : m) (c : α) (x : m → α),
  (Matrix.single i j c).mulVec x = Function.update 0 i (c * x j)
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_imK : Continuous fun q => q.imK
-- Init.Core
/-- Decidable equality for Empty  -/
instDecidableEqEmpty : DecidableEq Empty
-- Mathlib.LinearAlgebra.BilinearForm.Basic
/-- `coeFn` as an `AddMonoidHom`  -/
LinearMap.BilinForm.coeFnAddMonoidHom : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M →+ M → M → R
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.PreDiscrTree.instAppend : {α : Type} → Append (Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
-- Mathlib.Combinatorics.Digraph.Basic
/-- The adjacency relation of a digraph.  -/
Digraph.Adj : {V : Type u_1} → Digraph V → V → V → Prop
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_singleton : ∀ {m n : ℤ}, n = m → (m...=n).toList = [m]
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The underlying object of `equalizerSubobject f g` is (up to isomorphism!)
the same as the chosen object `equalizer f g`.  -/
CategoryTheory.Limits.equalizerSubobjectIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasEqualizer f g] →
          CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.equalizerSubobject f g) ≅
            CategoryTheory.Limits.equalizer f g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_3 : Inhabited (γ k)],
  m.WF → (Std.DHashMap.Raw.filterMap f m).get! k = ((m.get? k).bind (f k)).get!
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.mk : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    (toLinearMap : L →ₗ[R] M) →
                      (∀ (a b : L), toLinearMap ⁅a, b⁆ = ⁅a, toLinearMap b⁆ - ⁅b, toLinearMap a⁆) → LieDerivation R L M
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_clearUnit_foldl : ∀ {α : Type u} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (f : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → α → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  (∀ (arr : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (a : α), (f arr a).size = arr.size) →
    ∀ (l : List α), (List.foldl f assignments l).size = assignments.size
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasureOnCompacts.smul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {c : ENNReal}, c ≠ ⊤ → MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.mk.inj : ∀ {A : Type u} {inst : Ring A} {G : Type w₀} {R : Type w₁} {relation : R → G →₀ A} {G_1 : Type w₀} {R_1 : Type w₁}
  {relation_1 : R_1 → G_1 →₀ A},
  { G := G, R := R, relation := relation } = { G := G_1, R := R_1, relation := relation_1 } →
    G = G_1 ∧ R = R_1 ∧ relation ≍ relation_1
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.tuple : List Lean.Parser.Tactic.MCasesPat → Lean.Parser.Tactic.MCasesPat
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Week.Aligned.Ordinal
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, Meromorphic f → Meromorphic (-f)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo.congr_simp : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i i_1 : M →ₗ[R] N) (e_i : i = i_1) (f f_1 : M →ₗ[R] Q),
  f = f_1 →
    ∀ [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) (y y_1 : N),
      y = y_1 →
        Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y =
          Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i_1 f_1 h y_1
-- Lean.Meta.Sym.Eta
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.etaReduceAux.go : ℕ → Lean.Expr → Lean.Expr → ℕ → ℕ → Lean.Expr
-- Init.Data.BitVec.Lemmas
BitVec.cpop_concat : ∀ {w : ℕ} {x : BitVec w} {b : Bool}, (x.concat b).cpop = ↑b.toNat + BitVec.setWidth (w + 1) x.cpop
-- Init.Data.Int.Lemmas
Int.sub_self : ∀ (a : ℤ), a - a = 0
-- Mathlib.Algebra.Module.Submodule.Defs
/-- The carrier set is closed under scalar multiplication.  -/
Submodule.smul_mem' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (self : Submodule R M)
  (c : R) {x : M}, x ∈ self.carrier → c • x ∈ self.carrier
-- Mathlib.GroupTheory.Commutator.Basic
/-- The commutator of two additive subgroups `H₁` and `H₂`.  -/
AddSubgroup.addCommutator : {G : Type u_1} → [inst : AddGroup G] → Bracket (AddSubgroup G) (AddSubgroup G)
-- Mathlib.GroupTheory.GroupAction.Quotient
ConjClasses.card_carrier : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] (g : G) [inst_2 : Fintype ↑(ConjClasses.mk g).carrier]
  [inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)],
  Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I : Ideal R}, ↑I ≠ 0 ↔ I ≠ ⊥
-- Mathlib.Algebra.Group.Defs
npowRecAuto.eq_1 : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] (k : ℕ) (m : M), npowRecAuto k m = npowRec k m
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
Matrix.SpecialLinearGroup.lineStab_isMulCommutative_of_span : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (v : ι → F),
  v ≠ 0 → IsMulCommutative ↥(Matrix.SpecialLinearGroup.lineStab (F ∙ v))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_μ_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X Y : C), (CategoryTheory.Functor.LaxMonoidal.μ (F.prod' G) X Y).2 = CategoryTheory.Functor.LaxMonoidal.μ G X Y
-- Mathlib.Algebra.Group.Units.Defs
Units.mk : {α : Type u} → [inst : Monoid α] → (val inv : α) → val * inv = 1 → inv * val = 1 → αˣ
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- An alias of `ContinuousMultilinearMap.seminormedAddCommGroup` with non-dependent types to help
typeclass search.  -/
ContinuousMultilinearMap.seminormedAddCommGroup' : {𝕜 : Type u} →
  {ι : Type v} →
    {G : Type wG} →
      {G' : Type wG'} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup G] →
            [inst_2 : NormedSpace 𝕜 G] →
              [inst_3 : SeminormedAddCommGroup G'] →
                [inst_4 : NormedSpace 𝕜 G'] →
                  [Fintype ι] → SeminormedAddCommGroup (ContinuousMultilinearMap 𝕜 (fun x => G) G')
-- Mathlib.Data.Set.Lattice.Image
Set.image_projection_prod : ∀ {ι : Type u_9} {α : ι → Type u_10} {v : (i : ι) → Set (α i)},
  (Set.univ.pi v).Nonempty → ∀ (i : ι), (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k = v i
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.eq_inv_mul_iff_mul_eq : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit b → (a = b⁻¹ * c ↔ b * a = c)
-- Init.Data.String.Lemmas.Modify
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this.  -/
String.Pos.Splits.pastSet : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String} {c d : Char} (h : p.Splits t₁ (String.singleton c ++ t₂)),
  (p.pastSet d ⋯).Splits (t₁ ++ String.singleton d) t₂
-- Mathlib.Topology.Constructions.SumProd
continuousAt_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X × Y},
  ContinuousAt Prod.snd p
-- Mathlib.Tactic.Ring.Compare
/-- In a commutative semiring, given `Ring.ExSum` objects `va`, `vb` which differ by a positive
(additive) constant, construct a proof of `$a < $b`, where `a` (resp. `b`) is the expression in the
semiring to which `va` (resp. `vb`) evaluates.  -/
Mathlib.Tactic.Ring.evalLE : {v : Lean.Level} →
  {α : Q(Type v)} →
    (ics : Q(CommSemiring «$α»)) →
      (x : Q(PartialOrder «$α»)) →
        Q(IsOrderedRing «$α») →
          {a b : Q(«$α»)} →
            Mathlib.Tactic.Ring.ExSum q(«$ics») a →
              Mathlib.Tactic.Ring.ExSum q(«$ics») b → Lean.MetaM (Except Mathlib.Tactic.Ring.ExceptType Q(«$a» ≤ «$b»))
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.lt_of_st_lt : ∀ {x y : ℝ*}, ¬x.Infinite → ¬y.Infinite → x.st < y.st → x < y
-- Init.SimpLemmas
forall_congr : ∀ {α : Sort u} {p q : α → Prop}, (∀ (a : α), p a = q a) → (∀ (a : α), p a) = ∀ (a : α), q a
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.X_pow_smul_rTensor_monomial : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (k : ℕ) (sn : TensorProduct R S N),
  Polynomial.X ^ k • (LinearMap.rTensor N (↑R (Polynomial.monomial 0))) sn =
    (LinearMap.rTensor N (↑R (Polynomial.monomial k))) sn
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_sUnion_of_directed : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set (Set A)},
  s.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) s →
      (∀ a ∈ s, AlgebraicIndependent R Subtype.val) → AlgebraicIndependent R Subtype.val
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.natTransCommShift_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type u_3}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁]
  [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) [inst_8 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_9 : CategoryTheory.HasShift D₁ M] [inst_10 : CategoryTheory.HasShift D₂ M]
  [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M] (G : CategoryTheory.Functor D₁ D₂)
  (e : Φ.functor.comp L₂ ≅ L₁.comp G), CategoryTheory.NatTrans.CommShift e.hom M
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.coe_quotEquivOfEqBot_symm : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (hp : p = ⊥), ↑(p.quotEquivOfEqBot hp).symm = p.mkQ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.pred.sizeOf_spec : ∀ (q₁ q₂ : Turing.PartrecToTM2.Λ'), sizeOf (q₁.pred q₂) = 1 + sizeOf q₁ + sizeOf q₂
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- If `c` is a pullback cone, then `c.op.unop` is isomorphic to `c`.  -/
CategoryTheory.Limits.PullbackCone.opUnopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} → {f : X ⟶ Z} → {g : Y ⟶ Z} → (c : CategoryTheory.Limits.PullbackCone f g) → c.op.unop ≅ c
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isOpen_setOfPred_disjoint_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], IsOpen {p | Disjoint ↑p.1 ↑p.2}
-- Mathlib.Topology.Order.IsLUB
IsGLB.frequently_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsGLB s a → s.Nonempty → ∃ᶠ (x : α) in nhdsWithin a (Set.Ici a), x ∈ s
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.toIntAlgEquiv_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S], Function.Injective RingEquiv.toIntAlgEquiv
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Config.mk.injEq : ∀ (transparency : Lean.Meta.TransparencyMode) (occs : Lean.Meta.Occurrences)
  (castMode : Mathlib.Tactic.DepRewrite.CastMode) (castTransparency transparency_1 : Lean.Meta.TransparencyMode)
  (occs_1 : Lean.Meta.Occurrences) (castMode_1 : Mathlib.Tactic.DepRewrite.CastMode)
  (castTransparency_1 : Lean.Meta.TransparencyMode),
  ({ transparency := transparency, occs := occs, castMode := castMode, castTransparency := castTransparency } =
      { transparency := transparency_1, occs := occs_1, castMode := castMode_1,
        castTransparency := castTransparency_1 }) =
    (transparency = transparency_1 ∧ occs = occs_1 ∧ castMode = castMode_1 ∧ castTransparency = castTransparency_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The second part of the third simplicial identity  -/
SimplexCategory.δ_comp_σ_succ : ∀ {n : ℕ} {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) (SimplexCategory.σ i) =
    CategoryTheory.CategoryStruct.id { len := n }
-- Init.Data.List.Basic
/-- Drops the first element of a nonempty list, returning the tail. Returns `[]` when the argument is
empty.

Examples:
 * `["apple", "banana", "grape"].tail = ["banana", "grape"]`
 * `["apple"].tail = []`
 * `([] : List String).tail = []`
 -/
List.tail : {α : Type u} → List α → List α
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.toHasIntCast : {R : Type u} →
  {S : Type v} → [inst : NonAssocRing R] → [inst_1 : SetLike S R] → [hSR : SubringClass S R] → (s : S) → IntCast ↥s
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `UniformCauchySeqOn.mul` -/
UniformCauchySeqOn.fun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (fun i i_1 => f i i_1 * f' i i_1) l s
-- Mathlib.Logic.Nontrivial.Basic
nontrivial_prod_left : ∀ {α : Type u_1} {β : Type u_2} [Nontrivial α] [Nonempty β], Nontrivial (α × β)
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The category of monomorphisms into `X` as a full subcategory of the over category.
This isn't skeletal, so it's not a partial order.

Later we define `Subobject X` as the quotient of this by isomorphisms.
 -/
CategoryTheory.MonoOver : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max u₁ v₁)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instPartialOrder : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenNormalSubgroup G)
-- Init.Data.Nat.Basic
Nat.ge_of_not_lt : ∀ {n m : ℕ}, ¬n < m → n ≥ m
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.liftFromOverComp.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.WithTerminal J → Sort u_2) (a : J)
  (h_1 : Unit → motive CategoryTheory.WithTerminal.star) (h_2 : (a : J) → motive (CategoryTheory.WithTerminal.of a)),
  (match CategoryTheory.WithTerminal.of a with
    | CategoryTheory.WithTerminal.star => h_1 ()
    | CategoryTheory.WithTerminal.of a => h_2 a) =
    h_2 a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.type : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Expr → autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1 → Lean.Compiler.LCNF.Arg pu
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro
/-- Given a projective resolution `P` of `k` as a `k`-linear `G`-representation, a subgroup
`S ≤ G`, and a `k`-linear `S`-representation `A`, this is an isomorphism of complexes
`(A ⊗ Res(S)(P))_S ≅ (Ind_S^G(A) ⊗ P)_G`.  -/
groupHomology.coinvariantsTensorResProjectiveResolutionIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (S : Subgroup G) →
        (A : Rep.{u, u, u} k ↥S) →
          (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) →
            HomologicalComplex.coinvariantsTensorObj A ((Rep.resFunctor S.subtype).mapProjectiveResolution P).complex ≅
              HomologicalComplex.coinvariantsTensorObj (Rep.ind S.subtype A) P.complex
-- Std.Async.System
Std.Async.System.instDecidableEqCPUTimes.decEq : (x x_1 : Std.Async.System.CPUTimes) → Decidable (x = x_1)