mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_hom_apply_1 : ∀ {X Y Z : Type u}
  {x :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).1 = x.1.1
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.add_one_le_of_lt : ∀ {n m : WithBot ℕ}, n < m → n + 1 ≤ m
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- The underlying map `B → M` of a derivation `M.Derivation f` when `M : ModuleCat B`
and `f : A ⟶ B` is a morphism in `CommRingCat`.  -/
ModuleCat.Derivation.d : {A B : CommRingCat} → {M : ModuleCat ↑B} → {f : A ⟶ B} → M.Derivation f → ↑B → ↑M
-- Init.Data.Char.Ordinal
Char.val_ofOrdinal : ∀ {f : Fin Char.numCodePoints},
  (Char.ofOrdinal f).val = if h : ↑f < 55296 then UInt32.ofNatLT ↑f ⋯ else UInt32.ofNatLT (↑f + Char.numSurrogates) ⋯
-- Mathlib.Order.Interval.Finset.DenselyOrdered
LocallyFiniteOrder.denselyOrdered_iff_subsingleton : ∀ {X : Type u_1} [inst : LinearOrder X] [LocallyFiniteOrder X], DenselyOrdered X ↔ Subsingleton X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.Const.insertMany t l) k =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if cmp a k = Ordering.eq then some b else none)
          l).or
      (Std.DTreeMap.Const.get? t k)
-- Mathlib.Analysis.Convolution
/-- A sufficient condition to prove that `f ⋆[L, μ] g` exists.
We assume that `f` is integrable on a set `s` and `g` is bounded and ae strongly measurable
on `x₀ - s` (note that both properties hold if `g` is continuous with compact support).  -/
BddAbove.convolutionExistsAt' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd G] [MeasurableNeg G] {x₀ : G} {s : Set G},
  BddAbove ((fun i => ‖g i‖) '' (fun t => -t + x₀) ⁻¹' s) →
    MeasurableSet s →
      (Function.support fun t => (L (f t)) (g (x₀ - t))) ⊆ s →
        MeasureTheory.IntegrableOn f s μ →
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x₀ - t) (μ.restrict s)) →
            MeasureTheory.ConvolutionExistsAt f g x₀ L μ
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.dropEndWhile_char_eq_dropEndWhile_beq : ∀ {c : Char} {s : String.Slice}, s.dropEndWhile c = s.dropEndWhile fun x => x == c
-- Mathlib.Probability.Kernel.Category.SFinKer
/-- The underlying measurable space.  -/
SFinKer.carrier : SFinKer → Type u
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Summation (i.e., `tsum`) in `ℓ¹(α, E)` as a continuous linear map.  -/
lp.tsumCLM : (𝕜 : Type u_1) →
  (α : Type u_3) →
    (E : Type u_5) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedRing 𝕜] →
          [inst_2 : Module 𝕜 E] → [inst_3 : IsBoundedSMul 𝕜 E] → [CompleteSpace E] → ↥(lp (fun x => E) 1) →L[𝕜] E
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.δ_fromSingleMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (n' q' : ℤ) (h' : p + n' = q'),
  CochainComplex.HomComplex.δ n n' (CochainComplex.HomComplex.Cochain.fromSingleMk f h) =
    CochainComplex.HomComplex.Cochain.fromSingleMk (CategoryTheory.CategoryStruct.comp f (K.d q q')) h'
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_support_iff_not_isIsolated : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, v ∈ G.support ↔ ¬G.IsIsolated v
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X x x_1 : D) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    e.functor.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (e.inverse.obj X) (e.inverse.map f))
-- Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
/-- The wide pullback cone given by a fan, when the base object is terminal.  -/
CategoryTheory.Limits.WidePullbackCone.ofFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      {B : C} →
        {objs : ι → C} →
          (arrows : (j : ι) → objs j ⟶ B) →
            CategoryTheory.Limits.Fan objs →
              CategoryTheory.Limits.IsTerminal B → CategoryTheory.Limits.WidePullbackCone arrows
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eraseLead' : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} {c : ℕ}, f.support.card = c + 1 → f.eraseLead.support.card = c
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.sheafCompose_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  {F : CategoryTheory.Functor A B} [inst_3 : J.HasSheafCompose F],
  CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.sheafCompose J F)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_zsmul_add_eq_zero_of_sign_eq : ∀ {θ ψ : Real.Angle}, 2 • (θ + ψ) = 0 → θ.sign = ψ.sign → θ.sign ≠ 0 → |θ.toReal| + |ψ.toReal| = Real.pi
-- Init.Data.Int.DivMod.Lemmas
Int.neg_ediv : ∀ {a b : ℤ}, -a / b = -(a / b) - if b ∣ a then 0 else b.sign
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_zero_interval : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], ↑0 = 0
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `1` is the homomorphism sending all elements to `1`.  -/
OrderMonoidHom.instOne : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : MulOneClass α] → [inst_3 : MulOneClass β] → One (α →*o β)
-- Mathlib.Data.Set.Lattice
Set.biUnion_mono : ∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t t' : α → Set β},
  s' ⊆ s → (∀ x ∈ s, t x ⊆ t' x) → ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorphOn.preimage_boundary_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 →
    ∀ {f : M → N} {s : Set M},
      IsLocalDiffeomorphOn I I' n f s → f ⁻¹' ModelWithCorners.boundary N ∩ s = ModelWithCorners.boundary M ∩ s
-- Mathlib.Order.CountableSupClosed
/-- **Alias** of the reverse direction of `countableSupClosure_eq_self`. -/
CountableSupClosed.countableSupClosure_eq : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], CountableSupClosed s → countableSupClosure s = s
-- Init.Data.Nat.Lemmas
Nat.mul_dvd_of_dvd_div : ∀ {a b c : ℕ}, c ∣ b → a ∣ b / c → c * a ∣ b
-- Mathlib.Order.Sublattice
/-- The top sublattice is isomorphic to the original lattice.

This is the sublattice version of `Equiv.Set.univ α`.  -/
Sublattice.topEquiv : {α : Type u_2} → [inst : Lattice α] → ↥⊤ ≃o α
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Given a bifunctor `G : C₁ ⥤ C₂ ⥤ C`, diagrams `K₁ : J₁ ⥤ C₁` and `K₂ : J₂ ⥤ C₂`, and cocones
over these diagrams, `G.mapCocone₂ c₁ c₂` is the cocone over the diagram `J₁ × J₂ ⥤ C` obtained
by applying `G` to both `c₁` and `c₂`.  -/
CategoryTheory.Functor.mapCocone₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                      {K₁ : CategoryTheory.Functor J₁ C₁} →
                        {K₂ : CategoryTheory.Functor J₂ C₂} →
                          CategoryTheory.Limits.Cocone K₁ →
                            CategoryTheory.Limits.Cocone K₂ →
                              CategoryTheory.Limits.Cocone
                                (CategoryTheory.Functor.uncurry.obj
                                  ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_max?_iff_ne_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t.max?.isSome = true ↔ t ≠ ∅
-- Mathlib.Order.Fin.Finset
Fin.orderIsoPair_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableEq α] (a b : α) (hab : a < b),
  ↑((Fin.orderIsoPair a b hab) 0) = a
-- Mathlib.Analysis.Normed.Group.Hom
/-- The image of a bounded group homomorphism. Naturally endowed with a
`SeminormedAddCommGroup` instance.  -/
NormedAddGroupHom.range : {V₁ : Type u_3} →
  {V₂ : Type u_4} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → AddSubgroup V₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.unitOfList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeMap.Raw.unitOfList [] cmp = ∅
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_a₂_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).a₂ = W.a₂
-- Mathlib.Logic.Basic
by_cases : ∀ {p q : Prop}, (p → q) → (¬p → q) → q
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `truth C` is a regular monomorphism (because it is split).  -/
CategoryTheory.HasSubobjectClassifier.truthIsRegularMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasSubobjectClassifier C] →
      CategoryTheory.RegularMono (CategoryTheory.HasSubobjectClassifier.truth C)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mk : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      {a : α} → (parts : Finset α) → parts.SupIndep id → parts.sup id = a → ⊥ ∉ parts → Finpartition a
-- Mathlib.Analysis.Convolution
MeasureTheory.posConvolution_eq_convolution_indicator : ∀ {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ E'] [inst_5 : NormedSpace ℝ F]
  (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F)
  (ν : autoParam (MeasureTheory.Measure ℝ) MeasureTheory.posConvolution_eq_convolution_indicator._auto_1)
  [MeasureTheory.NullSingletonClass ν],
  MeasureTheory.posConvolution f g L ν =
    MeasureTheory.convolution ((Set.Ioi 0).indicator f) ((Set.Ioi 0).indicator g) L ν
-- Mathlib.Order.SuccPred.WithBot
WithTop.pred_strictMono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] [NoMinOrder α],
  StrictMono WithTop.pred
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.entryAtIdx!_eq_getElem! : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced → ∀ {i : ℕ} [inst : Inhabited ((a : α) × β a)], t.entryAtIdx! i = t.toListModel[i]!
-- Std.Http.Data.Body.Stream
/-- Sends a chunk.

If `incomplete := true`, the chunk is buffered and collapsed with subsequent chunks, and is not
delivered to the receiver yet.
If `incomplete := false`, any buffered incomplete pieces are collapsed with this chunk and the
single merged chunk is sent.
 -/
Std.Http.Body.Stream.send : Std.Http.Body.Stream → Std.Http.Chunk → optParam Bool false → Std.Async.Async Unit
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
/-- The canonical identification between the tangent bundle to the model space and the product,
as a diffeomorphism.  -/
tangentBundleModelSpaceDiffeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (n : ℕ∞) →
                  Diffeomorph I.tangent (I.prod (modelWithCornersSelf 𝕜 E)) (TangentBundle I H) (ModelProd H E) ↑n
-- Mathlib.Order.Defs.LinearOrder
le_imp_le_of_lt_imp_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : LinearOrder β] {a b : α} {c d : β},
  (d < c → b < a) → a ≤ b → c ≤ d
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β] (f : α → β),
  Finset.inf 0 f = f 0
-- Mathlib.Topology.Algebra.Monoid
/-- The (topological-space) closure of a subsemigroup of a space `M` with `ContinuousMul` is
itself a subsemigroup.  -/
Subsemigroup.topologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] → [inst_1 : Semigroup M] → [SeparatelyContinuousMul M] → Subsemigroup M → Subsemigroup M
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.congr : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f g : α → ε},
  MeasureTheory.HasFiniteIntegral f μ → f =ᵐ[μ] g → MeasureTheory.HasFiniteIntegral g μ
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_pos : ∀ {q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], 0 < ↑q ↔ 0 < q
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMulActionOreLocalization.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X],
  OreLocalization.instMulActionOreLocalization = { toSMul := OreLocalization.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.lintegral_ofReal_ne_top_iff_integrable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    0 ≤ᵐ[μ] f → (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.exists_path_through_family' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ} {s : Set X},
  IsPathConnected s →
    ∀ (p : Fin (n + 1) → X),
      (∀ (i : Fin (n + 1)), p i ∈ s) → ∃ γ t, (∀ (t : ↑unitInterval), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
-- Mathlib.Analysis.Complex.Circle
Real.probChar_apply' : ∀ (x : ℝ), Real.probChar x = Circle.exp x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z), CategoryTheory.Limits.HasPullback f g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.type.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (expr : Lean.Expr)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1) (expr_1 : Lean.Expr)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Arg._auto_1),
  (Lean.Compiler.LCNF.Arg.type expr h = Lean.Compiler.LCNF.Arg.type expr_1 h_1) = (expr = expr_1)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.div_smul : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (a : A)
  (f : PowerSeries A) [inst_1 : IsAdicComplete I A], H.div (a • f) = a • H.div f
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supported.eq_1 : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M),
  AddMonoidAlgebra.supported R S s = Submodule.comap (↑(AddMonoidAlgebra.coeffLinearEquiv R)) (Finsupp.supported S R s)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.id_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C),
  (CategoryTheory.CategoryStruct.id T).toNatTrans = CategoryTheory.CategoryStruct.id T.toFunctor
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cosPartialEquiv_source : Real.cosPartialEquiv.source = Set.Icc 0 Real.pi
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forall_mem_toArray_iff_forall_mem_get : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {p : α → Prop}, m.WF → ((∀ k ∈ m.toArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h))
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.map_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {K' : Type u_5} [inst_5 : Field K'] [inst_6 : Algebra R₁ K']
  [inst_7 : IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K'),
  FractionalIdeal.map (↑h) I⁻¹ = (FractionalIdeal.map (↑h) I)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.rightUnitor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : CategoryTheory.Center C) → X.tensorObj CategoryTheory.Center.tensorUnit ≅ X
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.whiskering_linearCoyoneda : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C],
  (CategoryTheory.linearCoyoneda R C).comp
      ((CategoryTheory.Functor.whiskeringRight C (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) =
    CategoryTheory.coyoneda
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDerivWithin_cosh_Icc : ∀ (n : ℕ) {a b : ℝ},
  a < b → ∀ {x : ℝ}, x ∈ Set.Icc a b → iteratedDerivWithin n Real.cosh (Set.Icc a b) x = iteratedDeriv n Real.cosh x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Some factorisation of `f` through a monomorphism (selected with choice).  -/
CategoryTheory.Limits.Image.monoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasImage f] → CategoryTheory.Limits.MonoFactorisation f
-- Batteries.Data.Fin.Basic
/-- `find? p` returns the first `i` for which `p i = true`, or `none` if no such element is found.
The function `p` is not evaluated on further inputs after the first `i` is found.
 -/
Fin.find? : {n : ℕ} → (Fin n → Bool) → Option (Fin n)
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.mk.sizeOf_spec : ∀ (offset : Std.Time.TimeZone.Offset) (name abbreviation : String) (isDST : Bool),
  sizeOf { offset := offset, name := name, abbreviation := abbreviation, isDST := isDST } =
    1 + sizeOf offset + sizeOf name + sizeOf abbreviation + sizeOf isDST
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (X : J),
  (d.transitionCocone hij).ι.app X = CategoryTheory.CategoryStruct.comp ((d.trans hij).app X) ((d.cocone j).ι.app X)
-- Std.Time.Format.Modifier
/-- `O`: Localized zone offset using the `GMT` prefix (e.g., `GMT+8`, `GMT+08:00`).
 -/
Std.Time.Modifier.O : Std.Time.OffsetO → Std.Time.Modifier
-- Mathlib.Order.Filter.Defs
Filter.prod_eq_inf : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β),
  f ×ˢ g = Filter.comap Prod.fst f ⊓ Filter.comap Prod.snd g
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHomClass.instCoeTCStarAlgHom : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Star A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] → [AlgHomClass F R A B] → [StarHomClass F A B] → CoeTC F (A →⋆ₐ[R] B)
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getKey?` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getKey?ₘ : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Option α
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.mk.sizeOf_spec : ∀ (len : ℕ), sizeOf { len := len } = 1 + sizeOf len
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
IsDedekindDomain.HeightOneSpectrum.ofPrime.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {p p_1 : Ideal R} (e_p : p = p_1) (hp : Prime p),
  IsDedekindDomain.HeightOneSpectrum.ofPrime hp = IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_lt_of_lt : ∀ {m n : ℕ}, 0 < n → n < m → n.factorial < m.factorial
-- Mathlib.ModelTheory.Semantics
/-- A model of a theory is a structure in which every sentence is realized as true.  -/
FirstOrder.Language.Theory.Model : {L : FirstOrder.Language} → (M : Type w) → [L.Structure M] → L.Theory → Prop
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has limits then any reflective subcategory has limits.  -/
CategoryTheory.hasLimits_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C]
  [CategoryTheory.Reflective R], CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
-- Mathlib.Data.Nat.Size
Nat.size_one : Nat.size 1 = 1
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_sq_le_normSq : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.re z * RCLike.re z ≤ RCLike.normSq z
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_Ioo : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), (Finset.Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 2