mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- When `V` is a `R[M]`-module, multiplication by a group element `g` is a `R`-linear map.  -/
MonoidAlgebra.GroupSMul.linearMap : (R : Type u_1) →
  {M : Type u_7} →
    [inst : Monoid M] →
      [inst_1 : CommSemiring R] →
        (V : Type u_10) →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module R V] →
              [inst_4 : Module (MonoidAlgebra R M) V] → [IsScalarTower R (MonoidAlgebra R M) V] → M → V →ₗ[R] V
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.SqLe.eq_1 : ∀ (a c b d : ℕ), Zsqrtd.SqLe a c b d = (c * a * a ≤ d * b * b)
-- Mathlib.Data.Finsupp.AList
/-- Converts an association list into a finitely supported function via `AList.lookup`, sending
absent keys to zero.  -/
AList.lookupFinsupp : {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → (AList fun _x => M) → α →₀ M
-- Lean.Parser.Types
Lean.Parser.FirstTokens.epsilon : Lean.Parser.FirstTokens
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.mk.sizeOf_spec : ∀ (ref id type : Lean.Syntax) (bi : Lean.BinderInfo),
  sizeOf { ref := ref, id := id, type := type, bi := bi } = 1 + sizeOf ref + sizeOf id + sizeOf type + sizeOf bi
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symmEquiv_symm_apply_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Mul P] [inst_1 : Mul Q] (h : Q ≃* P) (a : P),
  ((MulEquiv.symmEquiv P Q).symm h) a = h.symm a
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.pseudoZero_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C},
  0 = ⟦CategoryTheory.Over.mk 0⟧
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f 1 ≤ 1`.  -/
seminormFromBounded_one_le : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → seminormFromBounded' f 1 ≤ 1
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.dsimpImpl : Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.eq_2 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (m : ℕ) (h : m.succ ≤ n),
  Nat.anyTR.loop✝ n f m.succ h = (f (n - m.succ) ⋯ || Nat.anyTR.loop✝ n f m ⋯)
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The `PointedCone` constructed from a pointed `ConvexCone`.  -/
ConvexCone.toPointedCone : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → (C : ConvexCone R E) → C.Pointed → PointedCone R E
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.leftMulMatrix_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S), Function.Injective ⇑(Algebra.leftMulMatrix b)
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.IsCocomm.mk : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A],
  ↑(TensorProduct.comm R A A) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul → Coalgebra.IsCocomm R A
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_associated_iff : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {x y : α},
  Associated (normalize x) y ↔ Associated x y
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
/-- We can find equipartitions of arbitrary size.  -/
Finpartition.exists_equipartition_card_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) {n : ℕ},
  n ≠ 0 → n ≤ s.card → ∃ P, P.IsEquipartition ∧ P.parts.card = n
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_lt_of_surjective_not_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Surjective f → ¬Function.Injective f → Fintype.card β < Fintype.card α
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (it : Std.Iter α),
  Std.Rxi.Iterator.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next => Std.IterStep.yield { internalState := { next := Std.PRange.succ? next } } next
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (c : F), fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x
-- Mathlib.Order.Hom.Lattice
LatticeHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ),
  (LatticeHom.dual.symm f) a = f a
-- Std.Time.Time.PlainTime
/-- Creates a new `PlainTime` by adjusting the `minute` component to the given value.
 -/
Std.Time.PlainTime.withMinutes : Std.Time.PlainTime → Std.Time.Minute.Ordinal → Std.Time.PlainTime
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_whiskerLeft_assoc : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z_1 : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Z) h))
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget AddGrpCat)
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.snoc_snoc_swap : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x₁ x₂ y₁ y₂ : X}
  {hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₁}
  {hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₂}
  {hsaty₁ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₁ hsat₁).last y₁}
  {hsaty₂ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₂ hsat₂).last y₂},
  JordanHolderLattice.Iso (RelSeries.last s, x₁) (x₂, y₂) →
    JordanHolderLattice.Iso (x₁, y₁) (RelSeries.last s, x₂) →
      CompositionSeries.Equivalent ((RelSeries.snoc s x₁ hsat₁).snoc y₁ hsaty₁)
        ((RelSeries.snoc s x₂ hsat₂).snoc y₂ hsaty₂)
-- Mathlib.Topology.IsLocalHomeomorph
/-- A space that admits a local homeomorphism to a discrete space is itself discrete.  -/
IsLocalHomeomorph.comap_discreteTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → ∀ [DiscreteTopology Y], DiscreteTopology X
-- Init.Data.Fin.Lemmas
Fin.castAdd_castLT : ∀ {n : ℕ} (m : ℕ) (i : Fin (n + m)) (hi : ↑i < n), Fin.castAdd m (i.castLT hi) = i
-- Mathlib.Data.Set.Enumerate
_private.Mathlib.Data.Set.Enumerate.0.Set.enumerate.match_1.splitter : {α : Type u_1} →
  (motive : Set α → ℕ → Sort u_2) →
    (x : Set α) → (x_1 : ℕ) → ((s : Set α) → motive s 0) → ((s : Set α) → (n : ℕ) → motive s n.succ) → motive x x_1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, (Asymptotics.IsBigOWith c l f fun x => -g' x) ↔ Asymptotics.IsBigOWith c l f g'
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.pop.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} {a a_1 : σ → Option (Γ k) → σ},
  Turing.TM2to1.StAct.pop a = Turing.TM2to1.StAct.pop a_1 → a = a_1
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Normed space structure constructed from an `InnerProductSpace.Core` structure, adjusting the
topology to make sure it is defeq to an already existing topology.  -/
InnerProductSpace.Core.toNormedSpaceOfTopology : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          [cd : InnerProductSpace.Core 𝕜 F] →
            [tF : TopologicalSpace F] →
              [inst_3 : IsTopologicalAddGroup F] →
                [inst_4 : ContinuousConstSMul 𝕜 F] →
                  (h : ContinuousAt (fun v => inner 𝕜 v v) 0) →
                    (h' : Bornology.IsVonNBounded 𝕜 {v | RCLike.re (inner 𝕜 v v) < 1}) → NormedSpace 𝕜 F
-- Mathlib.CategoryTheory.Sites.Coverage
/-- Given any covering sieve `S` on `X` and a morphism `f : Y ⟶ X`, there exists
some covering sieve `T` on `Y` such that `T` factors through `S` along `f`.  -/
CategoryTheory.Coverage.pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (self : CategoryTheory.Coverage C) ⦃X Y : C⦄ (f : Y ⟶ X),
  ∀ S ∈ self.coverings X, ∃ T ∈ self.coverings Y, T.FactorsThruAlong S f
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_apply : ∀ {n : ℕ}, ArithmeticFunction.cardDistinctFactors n = n.primeFactorsList.dedup.length
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instNegOffset : Neg Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instCoeSortType.eq_1 : MonCat.instCoeSortType = { coe := MonCat.carrier }
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_add : ∀ {α : Type u_3} [inst : AddMonoid α] (s t : Multiset α) (comm : {x | x ∈ s + t}.Pairwise AddCommute),
  (s + t).noncommSum comm = s.noncommSum ⋯ + t.noncommSum ⋯
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.splitter : (motive : Int.Internal.Linear.Expr → Sort u_1) →
  (x : Int.Internal.Linear.Expr) →
    ((a b : Int.Internal.Linear.Expr) → motive (a.add b)) →
      ((a b : Int.Internal.Linear.Expr) → motive (a.sub b)) →
        ((a : Int.Internal.Linear.Expr) → motive a.neg) →
          ((k : ℤ) → motive (Int.Internal.Linear.Expr.num k)) →
            ((v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v)) →
              ((k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e)) →
                ((e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)) → motive x
-- Lean.Meta.Sym.ExprPtr
_private.Lean.Meta.Sym.ExprPtr.0.Lean.Meta.Sym.isSameExpr.unsafe_impl_2 : Lean.Expr → Lean.Expr → Bool
-- Batteries.Control.AlternativeMonad
AlternativeMonad.toAlternative : {m : Type u_1 → Type u_2} → [self : AlternativeMonad m] → Alternative m
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.instCategoryPresheaf : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : TopCat) → CategoryTheory.Category.{max v w, max (max u v) w} (TopCat.Presheaf C X)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.role.bracketed : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instPartialOrder : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → PartialOrder (ConvexCone R M)
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_int8ToBitVec : ∀ (x : Int8), Int16.ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_one : ∀ {M : Type u_4} [inst : AddMonoid M], WithZero.log 1 = 0
-- Init.Data.List.Sublist
List.IsPrefix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.Sublist l₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ι_normalizedChainComplexMap_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {n : ℕ}
  (x : X.obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) ((SSet.normalizedChainComplexMap f R).f n) =
    Y.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)
-- Mathlib.Logic.Function.Defs
Function.uncurry_bicompr : ∀ {α : Type u_6} {β : Type u_7} {γ : Sort u_8} {δ : Sort u_9} (f : α → β → γ) (g : γ → δ),
  Function.uncurry (Function.bicompr g f) = g ∘ Function.uncurry f
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.instIsEllipticHSMulVariableChange : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) [W.IsElliptic],
  (C • W).IsElliptic
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.PlausibleStep.yield : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    it.internalState.dropping = false →
      Std.Iterators.Types.DropWhile.PlausibleStep it
        (Std.IterStep.yield (Std.IterM.Intermediate.dropWhileWithPostcondition P false it') out)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.append.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (bs : List α) (h_1 : (bs : List α) → motive [] bs)
  (h_2 : (a : α) → (as bs : List α) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Note that this provides `IsScalarTower S R R` which is needed by `smul_mul_assoc`.  -/
Subalgebra.isScalarTower_left : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {α : Type u_1} {β : Type u_2} [inst_3 : SMul α β] [inst_4 : SMul A α] [inst_5 : SMul A β] [IsScalarTower A α β],
  IsScalarTower (↥S) α β
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.coherentTopology.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C],
  CategoryTheory.coherentTopology C = CategoryTheory.coherentTopology C
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
/-- A category with an initial object and binary coproducts has a natural monoidal structure.  -/
CategoryTheory.monoidalOfHasFiniteCoproducts : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasInitial C] →
      [CategoryTheory.Limits.HasBinaryCoproducts C] → CategoryTheory.MonoidalCategory C
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getLE? k = t₂.getLE? k
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.startsWith pat = false → s.dropWhile pat = s
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instIsRightAdjointTopCatToContinuousGeneratedByCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  (TopCat.toContinuousGeneratedByCat X).IsRightAdjoint
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_succ_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀],
  0 ≤ a → ∀ (n : ℕ), 0 ≤ a ^ (n + 1)
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_umod : ∀ {w i : ℕ} {n d : BitVec w},
  (n % d).getMsbD i =
    if d = 0#w then n.getMsbD i else (BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w)).r.getMsbD i
-- Lean.Elab.SetOption
_private.Lean.Elab.SetOption.0.Lean.Elab.validateOptionValue.throwMistypedOptionValue : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Name → Lean.DataValue → Lean.DataValue → m Unit
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsOneApply.one_apply`. -/
one_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : One β}
  {inst_2 : One F} [self : IsOneApply F α β] (x : α), 1 x = 1
-- Aesop.Rule.Forward
/-- The theorem from which this rule is derived.  -/
Aesop.ForwardRule.term : Aesop.ForwardRule → Aesop.RuleTerm
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- `Finsupp.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
in `f`, as a bilinear map of `v` and `f`.
In the absence of `SMulCommClass R S M`, use `Finsupp.linearCombination`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
 -/
Finsupp.bilinearCombination : {α : Type u_1} →
  {M : Type u_2} →
    (R : Type u_5) →
      (S : Type u_6) →
        [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] → (α → M) →ₗ[S] (α →₀ R) →ₗ[R] M
-- Mathlib.Order.Height
Set.finite_of_chainHeight_ne_top : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s → s.chainHeight r ≠ ⊤ → s.Finite
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams.mk.inj : ∀ {textDocument : Lean.Lsp.TextDocumentIdentifier} {text? : Option String}
  {textDocument_1 : Lean.Lsp.TextDocumentIdentifier} {text?_1 : Option String},
  { textDocument := textDocument, text? := text? } = { textDocument := textDocument_1, text? := text?_1 } →
    textDocument = textDocument_1 ∧ text? = text?_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {fallback : β}, (t.erase k).getD k fallback = fallback
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
/-- Shapiro's lemma: given a subgroup `S ≤ G` and an `S`-representation `A`, we have
`Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A).`  -/
groupCohomology.coindIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {S : Subgroup G} →
        (A : Rep.{u, u, u} k ↥S) →
          (n : ℕ) → groupCohomology (Rep.coind.{u, u, u, u} S.subtype A) n ≅ groupCohomology A n
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_of_subset_right : ∀ {α : Type u_2} {s t u : Finset α}, t ⊆ u → Disjoint s u → Disjoint s t
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.toCat_unit_toNatTrans : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G), adj.toCat.unit.toNatTrans = adj.unit
-- Mathlib.Algebra.Order.SuccPred.WithBot
WithBot.succ_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : AddMonoidWithOne α] [inst_3 : SuccAddOrder α],
  WithBot.succ 1 = 2
-- Mathlib.Logic.Relation
Relation.TransGen.mono : ∀ {α : Type u_1} {r p : α → α → Prop}, r ≤ p → Relation.TransGen r ≤ Relation.TransGen p
-- Init.Data.List.Basic
List.cons_lex_cons : ∀ {α : Type u} {lt : α → α → Bool} [inst : BEq α] {a b : α} {as bs : List α},
  (a :: as).lex (b :: bs) lt = (lt a b || a == b && as.lex bs lt)
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_shiftRight : ∀ (a b : UInt32), (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 32)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeMonoid α),
  FreeMonoid.toList ((FreeMonoid.map f) xs) = List.map f (FreeMonoid.toList xs)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_ofList_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (Std.DHashMap.Raw.ofList l).size ≤ l.length
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, Array.find? (fun x_2 => x_2.fst == k) m.toArray = none ↔ m.contains k = false
-- Lean.Compiler.NameMangling
Lean.mkModuleInitializationPrefix : Lean.IRPhases → String
-- Mathlib.Logic.Equiv.Defs
Equiv.left_inv : ∀ {α : Sort u_1} {β : Sort u_2} (self : α ≃ β), Function.LeftInverse self.invFun self.toFun
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_sq_eq : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [inst_6 : CStarModule A E] {x : E},
  ‖x‖ ^ 2 = ‖inner A x x‖
-- Mathlib.GroupTheory.Order.Min
AddMonoid.minOrder_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddTorsionFree G], AddMonoid.minOrder G = ⊤
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.span_le_span : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s t : Set (Projectivization K V)}, s ⊆ t → Projectivization.Subspace.span s ≤ Projectivization.Subspace.span t
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.mk.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (deg : ι) (num num_1 : ↥(𝒜 deg)),
  num = num_1 →
    ∀ (den den_1 : ↥(𝒜 deg)) (e_den : den = den_1) (den_mem : ↑den ∈ x),
      { deg := deg, num := num, den := den, den_mem := den_mem } =
        { deg := deg, num := num_1, den := den_1, den_mem := ⋯ }
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α},
  Coheyting.boundary a ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.IsCocomm.comm_comp_comul : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : Coalgebra R A} [self : Coalgebra.IsCocomm R A],
  ↑(TensorProduct.comm R A A) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.functor_obj_map : ∀ (n : Type uᵒᵖ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (AlgebraicGeometry.AffineSpace.functor.obj n).map f = AlgebraicGeometry.AffineSpace.map (Opposite.unop n) f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        (m₁.diff! m₂).get! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then default else m₁.get! k
-- Std.Data.HashSet.Lemmas
Std.HashSet.equiv_iff_forall_mem_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α],
  m₁.Equiv m₂ ↔ ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂
-- Mathlib.Algebra.Group.Ext
AddMonoid.ext_iff : ∀ {M : Type u} {m₁ m₂ : AddMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Mathlib.Topology.Algebra.InfiniteSum.Order
HasSum.nonneg : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} [L.NeBot],
  (∀ (i : ι), 0 ≤ g i) → HasSum g a L → 0 ≤ a
-- Mathlib.Tactic.GRewrite.Elab
/-- Return the union of `lctx₁` and `lctx₂`.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.mergeLCtx : Lean.LocalContext → Lean.LocalContext → Lean.LocalContext