mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDesc_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F G H : CategoryTheory.MonoidalCategory.DayFunctor C V}
  (α :
    CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor ⟶
      (CategoryTheory.MonoidalCategory.tensor C).comp H.functor)
  (x y : C),
  CategoryTheory.CategoryStruct.comp ((F.η G).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayFunctor.tensorDesc α).natTrans.app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    α.app (x, y)
-- Init.Data.List.Basic
List.instLawfulIdentityHAppendNil : ∀ {α : Type u}, Std.LawfulIdentity (fun x1 x2 => x1 ++ x2) []
-- Mathlib.Data.Finset.NAry
Finset.image_subset_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {b : β}, b ∈ t → Finset.image (fun a => f a b) s ⊆ Finset.image₂ f s t
-- Init.Data.UInt.Basic
/-- Bitwise and for 8-bit unsigned integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.land : UInt8 → UInt8 → UInt8
-- Mathlib.Order.Category.LinOrd
LinOrd.instInhabited : Inhabited LinOrd
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_le : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {P : Submodule R A},
  1 ≤ P ↔ 1 ∈ P
-- Mathlib.LinearAlgebra.Prod
/-- The map `(x, y) ↦ (-y, x)` as a linear equivalence.  -/
LinearEquiv.skewSwap : (R : Type u) →
  (M : Type v) →
    (N : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] → [inst_3 : Module R M] → [inst_4 : Module R N] → (M × N) ≃ₗ[R] N × M
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- We say `G` acts naturally on the fibers of `F` if for every `f : X ⟶ Y`, the `G`-actions
on `F.obj X` and `F.obj Y` are compatible with `F.map f`.  -/
CategoryTheory.PreGaloisCategory.IsNaturalSMul : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      (G : Type u_1) → [inst_1 : Group G] → [(X : C) → MulAction G (F.obj X).obj] → Prop
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `g : ℝ → ℝ` is periodic with period `T > 0` and `∀ x, 0 < g x`, then `t ↦ ∫ x in 0..t, g x`
tends to `∞` as `t` tends to `∞`.  -/
Function.Periodic.tendsto_atTop_intervalIntegral_of_pos' : ∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    IntervalIntegrable g MeasureTheory.volume 0 T →
      (∀ (x : ℝ), 0 < g x) → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atTop Filter.atTop
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Shortcut lemma for `Matrix.toLin'_mul` and `LinearMap.comp_apply`  -/
Matrix.toLin'_mul_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n]
  [inst_2 : Fintype n] [inst_3 : Fintype m] [inst_4 : DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) (x : n → R),
  (Matrix.toLin' (M * N)) x = (Matrix.toLin' M) ((Matrix.toLin' N) x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_max?_iff_isEmpty_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.max?.isSome = true ↔ t.isEmpty = false
-- Mathlib.LinearAlgebra.LinearDisjoint
Submodule.LinearDisjoint.of_subsingleton : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S}
  [Subsingleton R], M.LinearDisjoint N
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_coe : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] (f : ι →₀ M), ⇑f.toDFinsupp = ⇑f
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.symm_apply_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x : P₂} {y : P},
  e.symm x = y ↔ x = e y
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_neg : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p]
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.mk : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} →
        {e : J} →
          D.W (CategoryTheory.CategoryStruct.id e) →
            (lift : {j : J} → D.P j → (j ⟶ e)) →
              (∀ {j : J} (hj : D.P j), D.W (lift hj)) →
                (∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ) →
                  (∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯) →
                    D.IsTerminal e
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.h : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget aig w), 0 < self.len
-- Mathlib.Logic.Equiv.Sum
Equiv.sumAssoc_apply_inl_inl : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α), (Equiv.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
-- Lean.Attributes
Lean.TagAttribute.mk.sizeOf_spec : ∀ (attr : Lean.AttributeImpl) (ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet),
  sizeOf { attr := attr, ext := ext } = 1 + sizeOf attr + sizeOf ext
-- Mathlib.Order.UpperLower.Basic
isUpperSet_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (a : α), IsUpperSet (Set.Ioi a)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
/-- [Kerodon Tag 02MH](https://kerodon.net/tag/02MH) -/
SSet.nonDegenerate_δ : ∀ {X : SSet} [X.Nonsingular] {n : ℕ} {x : X.obj (Opposite.op { len := n + 1 })},
  x ∈ X.nonDegenerate (n + 1) →
    ∀ (i : Fin (n + 2)),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x ∈ X.nonDegenerate n
-- Mathlib.Topology.Sion
/-- **Alias** of `_private.Mathlib.Topology.Sion.0.Sion.isClosed_setOfPred_sublevelLeft_subset`.

---

Under suitable inequalities, `setOfPred_sublevelLeft_subset` is closed  -/
_private.Mathlib.Topology.Sion.0.Sion.isClosed_setOf_sublevelLeft_subset : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                  ∀ (a : E) (b b' : β) (y y' : ↑Y),
                    (∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')) →
                      (∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b) →
                        b' < max (f a ↑y) (f a ↑y') →
                          b < b' → IsClosed (Sion.setOfPred_sublevelLeft_subset✝ X Y f b b' y y')
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).X x =
    (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOver f S)
        (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f x) S)).left
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMaxEntryD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {fallback : α × β},
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.maxEntryD t₁ fallback = Std.DTreeMap.Raw.Const.maxEntryD t₂ fallback
-- Init.Data.List.Range
List.range_eq_nil : ∀ {n : ℕ}, List.range n = [] ↔ n = 0
-- Mathlib.Analysis.Quaternion
Quaternion.imJ_coeComplex : ∀ (z : ℂ), (↑z).imJ = 0
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSeparated f]
  [AlgebraicGeometry.IsSeparated g], AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- This instance asserts that if `G` has a left-cancellative multiplication, a linear order, and
multiplication is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueProds`.  -/
TwoUniqueProds.of_covariant_left : ∀ {G : Type u} [inst : Mul G] [IsLeftCancelMul G] [inst_2 : LinearOrder G] [MulRightStrictMono G], TwoUniqueProds G
-- Init.Data.List.Int.Sum
List.sum_reverse_int : ∀ (xs : List ℤ), xs.reverse.sum = xs.sum
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_strict_mono_of_ker_inf_eq : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Ring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂},
  p < p' → f.ker ⊓ p = f.ker ⊓ p' → Submodule.map f p < Submodule.map f p'
-- Lean.Parser.Extension
/-- Interpret `declName` if possible and inside a quotation, or else run `p`. The `ParserInfo` will always be taken from `p`.  -/
Lean.Parser.evalInsideQuot : Lean.Name → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Order.SuccPred.Archimedean
BddAbove.exists_isGreatest_of_nonempty : ∀ {X : Type u_3} [inst : LinearOrder X] [inst_1 : SuccOrder X] [IsSuccArchimedean X] {S : Set X},
  BddAbove S → S.Nonempty → ∃ x, IsGreatest S x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIso_hom : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) {P Q : CategoryTheory.Functor C₀ᵒᵖ A} (e : P ≅ Q),
  (data.multicospanMapIso e).hom = data.multicospanMap e.hom
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.checkCoeffDvd : Lean.Meta.Grind.Arith.CommRing.RingM Bool
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instIsStableUnderRetractsOppositeWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts],
  (HomotopicalAlgebra.weakEquivalences Cᵒᵖ).IsStableUnderRetracts
-- Mathlib.Topology.Algebra.LinearTopology
isLinearTopology_iff_hasBasis_ideal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R],
  IsLinearTopology R R ↔ (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0) fun I => ↑I
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G),
  G.IsRightDerivedFunctor β W ↔ CategoryTheory.IsIso (RF.rightDerivedDesc α W G β)
-- Mathlib.Topology.MetricSpace.Gluing
/-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a
space `GlueSpace hΦ hΨ` by identifying in `X ⊕ Y` the points `Φ x` and `Ψ x`.  -/
Metric.GlueSpace : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [Nonempty Z] →
        [inst : MetricSpace Z] →
          [inst_1 : MetricSpace X] →
            [inst_2 : MetricSpace Y] → {Φ : Z → X} → {Ψ : Z → Y} → Isometry Φ → Isometry Ψ → Type (max u v)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ)
  (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β),
  FirstOrder.Language.BoundedFormula.falsum.restrictFreeVar _f = FirstOrder.Language.BoundedFormula.falsum
-- Lean.Elab.Util
Lean.Elab.nestedExceptionToMessageData : {m : Type → Type} → [Monad m] → [Lean.MonadLog m] → Lean.Exception → m Lean.MessageData
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_eq_inf_of_coprime : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, I ⊔ J = ⊤ → I * J = I ⊓ J
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.comap_comap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] [inst_7 : AddCommMonoid O] [inst_8 : TopologicalSpace O] [inst_9 : Module R O] (g : N →L[R] O)
  (f : M →L[R] N) (s : ClosedSubmodule R O),
  ClosedSubmodule.comap f (ClosedSubmodule.comap g s) = ClosedSubmodule.comap (g ∘SL f) s
-- Aesop.Tree.Data
Aesop.MVarCluster.setParent : Option Aesop.RappRef → Aesop.MVarCluster → Aesop.MVarCluster
-- Mathlib.Data.EReal.Inv
EReal.bot_div_of_pos_ne_top : ∀ {a : EReal}, 0 < a → a ≠ ⊤ → ⊥ / a = ⊥
-- Mathlib.Data.List.Sort
List.sortedLE_iff_monotone_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE ↔ Monotone l.get
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.succ_mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [DecidableLT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo hi a : α},
  (Std.PRange.succ a ∈ (Std.PRange.succ lo)...Std.PRange.succ hi) ↔ a ∈ lo...hi
-- Mathlib.Data.Vector.Basic
/-- The recursive step of `scanl` splits a vector `x ::ᵥ v : Vector α (n + 1)`
into the provided starting value `b : β` and the recursed `scanl`
`f b x : β` as the starting value.

This lemma is the `cons` version of `scanl_get`.
 -/
List.Vector.scanl_cons : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n) (x : α),
  List.Vector.scanl f b (x ::ᵥ v) = b ::ᵥ List.Vector.scanl f (f b x) v
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : FreeAddMonoid α} {m : β},
  m ∈ (FreeAddMonoid.map f) a ↔ ∃ n ∈ a, f n = m
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.coxeterWeight_ne_four_of_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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) {i j : ι} [Finite ι]
  [NeZero 2] [IsAddTorsionFree M], LinearIndependent R ![P.root i, P.root j] → P.coxeterWeight i j ≠ 4
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_comap_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] (e : S ≃ₐ[R] S₁) (P : Ideal S₁),
  p.ramificationIdx' (Ideal.comap e P) = p.ramificationIdx' P
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.fullSymmetricSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) →
        [inst_2 : P.IsMonoidal] →
          [CategoryTheory.SymmetricCategory C] → CategoryTheory.SymmetricCategory P.FullSubcategory
-- Mathlib.RingTheory.DividedPowers.Padic
_private.Mathlib.RingTheory.DividedPowers.Padic.0.PadicInt.dividedPowers_eq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]),
  (PadicInt.dividedPowers p).dpow n x = if hx : x ∈ Ideal.span {↑p} then ⟨PadicInt.dpow'✝ p n ↑x, ⋯⟩ else 0
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftObj.unit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      Mathlib.Tactic.Coherence.LiftObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNew.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) l_1
-- Mathlib.Order.Defs.PartialOrder
lt_of_lt_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
-- Mathlib.Topology.UniformSpace.Defs
mem_nhds_uniformity_iff_left : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ {p | p.2 = x → p.1 ∈ s} ∈ uniformity α
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
/-- The currying operation `Hom ((toOver I).obj A) X → Hom A (I ⟹ X.left)`.  -/
CategoryTheory.Over.sectionsCurry : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {I : C} →
        [inst_2 : CategoryTheory.Closed I] →
          [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)] →
            [CategoryTheory.BraidedCategory C] →
              {X : CategoryTheory.Over I} →
                {A : C} → ((CategoryTheory.toOver I).obj A ⟶ X) → (A ⟶ (CategoryTheory.Over.sections I).obj X)
-- Mathlib.Topology.Order
instTopologicalSpaceFin : {n : ℕ} → TopologicalSpace (Fin n)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.coeFn_compLp' : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), ↑↑(L.compLp f) =ᵐ[μ] fun a => L (↑↑f a)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_pre_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A) {X Y : C}
  (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X) {Z : C} (h : B ⟹ X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry g)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app X) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalClosed.curry
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) g))
      h
-- Mathlib.RingTheory.Localization.Defs
IsLocalization'.mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S], M.IsLocalizationMap ⇑(algebraMap R S) → IsLocalization' M S
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.power_self_eq : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c ^ c = 2 ^ c
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain.  -/
AffineMap.mulAction : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : Module k V1] →
              [inst_3 : AddTorsor V1 P1] →
                [inst_4 : AddCommGroup V2] →
                  [inst_5 : Module k V2] →
                    {R : Type u_10} →
                      [inst_6 : Monoid R] →
                        [inst_7 : DistribMulAction R V2] → [SMulCommClass k R V2] → MulAction R (P1 →ᵃ[k] V2)