mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the forward direction of `Asymptotics.isTheta_const_smul_right`. -/
Asymptotics.IsTheta.of_const_smul_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : NormedSpace 𝕜 F'] {c : 𝕜},
  c ≠ 0 → (f =Θ[l] fun x => c • g' x) → f =Θ[l] g'
-- Mathlib.AlgebraicGeometry.PointsPi
/-- The canonical map `X(Π Rᵢ) ⟶ Π X(Rᵢ)`.
This is injective if `X` is quasi-separated, surjective if `X` is affine,
or if `X` is compact and each `Rᵢ` is local.  -/
AlgebraicGeometry.pointsPi : {ι : Type u} →
  (R : ι → CommRingCat) →
    (X : AlgebraicGeometry.Scheme) →
      (AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X) → (i : ι) → AlgebraicGeometry.Spec (R i) ⟶ X
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_not_contains_map_fst_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  l₁.isEmpty = true → (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁).isEmpty = true
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.forgetToTop_obj : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  AlgebraicGeometry.LocallyRingedSpace.forgetToTop.obj X =
    (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.equiv.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_5} [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M : Type u_6} {N : Type u_7}
  [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N] [inst_7 : Module R₂ N] (P : Submodule R M)
  (Q : Submodule R₂ N) (f f_1 : M ≃ₛₗ[σ₁₂] N) (e_f : f = f_1) (hf : Submodule.map (↑f) P = Q),
  Submodule.Quotient.equiv P Q f hf = Submodule.Quotient.equiv P Q f_1 ⋯
-- Mathlib.Order.Heyting.Basic
le_compl_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, a ≤ aᶜᶜ
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.instCoalgebraStruct : (R : Type u) →
  (ι : Type v) →
    (A : ι → Type w) →
      [DecidableEq ι] →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (A i)] →
            [inst_2 : (i : ι) → Module R (A i)] →
              [(i : ι) → CoalgebraStruct R (A i)] → CoalgebraStruct R (Π₀ (i : ι), A i)
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.costar_conj_star : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V)
  [inst_2 : Quiver.HasInvolutiveReverse U] [inst_3 : Quiver.HasInvolutiveReverse V] [φ.MapReverse] (u : U),
  φ.costar u = ⇑(Quiver.starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(Quiver.starEquivCostar u).symm
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_add_not_infinite : ∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.Infinite → (x + y).InfiniteNeg
-- Init.Data.Option.Lemmas
Option.some_beq_some : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, (some a == some b) = (a == b)
-- Mathlib.Data.Finsupp.Pointwise
/-- The pointwise multiplicative action of functions on finitely supported functions  -/
Finsupp.pointwiseModule : {α : Type u₁} → {β : Type u₂} → [inst : Semiring β] → Module (α → β) (α →₀ β)
-- Mathlib.Tactic.FunProp.Mor
/-- morphism coercion  -/
Mathlib.Meta.FunProp.Mor.App.coe : Mathlib.Meta.FunProp.Mor.App → Lean.Expr
-- Mathlib.Order.WithBot
WithTop.map_id : ∀ {α : Type u_1}, WithTop.map id = id
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f : X.fst ⟶ Y.fst)
  (comm :
    autoParam
      (∀ (U : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f U) (Y.snd.β U).hom =
          CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f))
      CategoryTheory.Center.Hom.comm._autoParam)
  (f_1 : X.fst ⟶ Y.fst)
  (comm_1 :
    autoParam
      (∀ (U : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f_1 U) (Y.snd.β U).hom =
          CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f_1))
      CategoryTheory.Center.Hom.comm._autoParam),
  ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Iic : ∀ (a : ENNReal), ENat.toENNReal ⁻¹' Set.Iic a = Set.Iic ⌊a⌋ₑ
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_surjective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Function.Injective ⇑f → Function.Surjective (Submonoid.comap f)
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            [LieAlgebra.IsKilling K L] →
              {H : LieSubalgebra K L} →
                [inst_5 : H.IsCartanSubalgebra] →
                  [LieModule.IsTriangularizable K (↥H) L] → InvolutiveNeg (LieModule.Weight K (↥H) L)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurable' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [SecondCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → Measurable τ
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instInhabitedSplitStatus : Inhabited Lean.Meta.Grind.SplitStatus
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N),
  (↑e).comp ↑e.symm = MonoidHom.id N
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.toOpenSubgroup : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → OpenNormalSubgroup G → OpenSubgroup G
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_σ₀Iter_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) (n : ℕ) {Z : C} (h : X.left.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ed.s' (CategoryTheory.CategoryStruct.comp (X.left.σ₀Iter n ⋯) h) =
    CategoryTheory.CategoryStruct.comp (ed.section_.app (Opposite.op { len := n })) h
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsColimit_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D), Subsingleton (CategoryTheory.Limits.ReflectsColimit K F)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_iSup_map_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f →
    ∀ {ι : Sort u_9} (S : ι → Submodule R M), Submodule.comap f (⨆ i, Submodule.map f (S i)) = iSup S
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Coloring.sumLeft_sum : ∀ {V : Type u_3} {W : Type u_5} {γ : Type u_7} {G : SimpleGraph V} {H : SimpleGraph W} (cG : G.Coloring γ)
  (cH : H.Coloring γ), (cG.sum cH).sumLeft = cG
-- Mathlib.Algebra.Module.SnakeLemma
SnakeLemma.δ'_eq : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) {K₃ : Type u_9} {C₁ : Type u_10} [inst_13 : AddCommGroup K₃]
  [inst_14 : Module R K₃] [inst_15 : AddCommGroup C₁] [inst_16 : Module R C₁] (ι₃ : K₃ →ₗ[R] M₃)
  (hι₃ : Function.Exact ⇑ι₃ ⇑i₃) (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⇑i₁ ⇑π₁) (hf₂ : Function.Surjective ⇑f₂)
  (hg₁ : Function.Injective ⇑g₁) (x : K₃) (y : M₂),
  f₂ y = ι₃ x →
    ∀ (z : N₁), g₁ z = i₂ y → (SnakeLemma.δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁) x = π₁ z
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.realFundSystem.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (i i_1 : Fin (NumberField.Units.rank K)),
  i = i_1 → NumberField.IsCMField.realFundSystem K i = NumberField.IsCMField.realFundSystem K i_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toArray_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {f : α → β → Bool},
  Std.DTreeMap.Const.toArray (Std.DTreeMap.filter f t) =
    Array.filter (fun p => f p.1 p.2) (Std.DTreeMap.Const.toArray t)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split_ineq_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (k b : ℤ) (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_left_split_ineq_cert p₁ p₂ k b p' =
    (p₂.leadCoeff.beq' b).and'
      (p'.beq' ((Int.Internal.Linear.Poly.combine_mul_k b (-p₁.leadCoeff) p₁.tail p₂.tail).addConst_k (b * k)))
-- Lean.Elab.App
Lean.Elab.Term.getElabElimInfo : Lean.Name → Lean.MetaM Lean.Elab.Term.ElabElimInfo
-- Mathlib.Data.Set.Finite.List
List.finite_length_lt : ∀ (α : Type u_1) [Finite α] (n : ℕ), {l | l.length < n}.Finite
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceContext.mk.injEq : ∀ (includeDeclaration includeDeclaration_1 : Bool),
  ({ includeDeclaration := includeDeclaration } = { includeDeclaration := includeDeclaration_1 }) =
    (includeDeclaration = includeDeclaration_1)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_inf : ∀ {R : Type u} [inst : NonAssocRing R] (p p' : Subring R), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- Assuming `α : R₀ ⟶ R.val` is the sheafification map of a presheaf of rings `R₀`
and `φ : M₀.presheaf ⟶ A.val` is the sheafification map of the underlying
sheaf of abelian groups of a presheaf of modules `M₀` over `R₀`, then given
`r : R.val.obj X` and `m : A.val.obj X`, this structure contains the data
of `x : A.val.obj X` along with the property which makes `x` a good candidate
for the definition of the scalar multiplication `r • m`.  -/
PresheafOfModules.Sheafify.SMulCandidate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (R₀ ⟶ R.obj) →
            {M₀ : PresheafOfModules R₀} →
              {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                (M₀.presheaf ⟶ A.obj) → {X : Cᵒᵖ} → ↑(R.obj.obj X) → ↑(A.obj.obj X) → Type v
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_on_Ioc' : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (z : ℤ),
  ∀ a ∈ Set.Ioc (↑z - 1) ↑z, ↑⌈a⌉ = ↑z
-- Mathlib.Data.WSeq.Basic
/-- Convert `s` to a list (if it is finite and completes in finite time).  -/
Stream'.WSeq.toList : {α : Type u} → Stream'.WSeq α → Computation (List α)
-- Mathlib.Data.List.Sort
List.sublist_of_subperm_of_pairwise : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] {l₁ l₂ : List α},
  l₁.Subperm l₂ → List.Pairwise r l₁ → List.Pairwise r l₂ → l₁.Sublist l₂
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {hom : S₁ ⟶ S₂} {inv : S₂ ⟶ S₁}
  {homotopyHomInvId :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom inv)
      (CategoryTheory.CategoryStruct.id S₁)}
  {homotopyInvHomId :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv hom)
      (CategoryTheory.CategoryStruct.id S₂)}
  {hom_1 : S₁ ⟶ S₂} {inv_1 : S₂ ⟶ S₁}
  {homotopyHomInvId_1 :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom_1 inv_1)
      (CategoryTheory.CategoryStruct.id S₁)}
  {homotopyInvHomId_1 :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv_1 hom_1)
      (CategoryTheory.CategoryStruct.id S₂)},
  { hom := hom, inv := inv, homotopyHomInvId := homotopyHomInvId, homotopyInvHomId := homotopyInvHomId } =
      { hom := hom_1, inv := inv_1, homotopyHomInvId := homotopyHomInvId_1, homotopyInvHomId := homotopyInvHomId_1 } →
    hom = hom_1 ∧ inv = inv_1 ∧ homotopyHomInvId ≍ homotopyHomInvId_1 ∧ homotopyInvHomId ≍ homotopyInvHomId_1
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.verify₁_eq_isSome_assemble₁ : ∀ {w : UInt8} {h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done},
  ByteArray.utf8DecodeChar?.verify₁ w h = (ByteArray.utf8DecodeChar?.assemble₁ w h).isSome
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforward_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y)
  (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  ((TopCat.Presheaf.pushforward C f).obj G).obj X_1 =
    G.obj (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop X_1)))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
PresheafOfModules.isSheaf_of_isLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {F : CategoryTheory.Functor D (PresheafOfModules R)}
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections]
  {c : CategoryTheory.Limits.Cone F} [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat]
  (hc : CategoryTheory.Limits.IsLimit c),
  (∀ (j : D), CategoryTheory.Presheaf.IsSheaf J (F.obj j).presheaf) → CategoryTheory.Presheaf.IsSheaf J c.pt.presheaf
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The `MulEquiv` between two monoids with a unique element.  -/
ContinuousMulEquiv.ofUnique : {M : Type u_3} →
  {N : Type u_4} →
    [Unique M] →
      [Unique N] →
        [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : TopologicalSpace M] → [inst_3 : TopologicalSpace N] → M ≃ₜ* N
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.contains_findCell : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered →
    Std.DTreeMap.Internal.Impl.contains' k l = true →
      (Std.DTreeMap.Internal.List.findCell l.toListModel k).contains = true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.inter_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.inter m₂ = m₁ ∩ m₂
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Stream.brecOn.go : {α : Type u_1} →
  {motive : RBTree.RBNode.Stream α → Sort u} →
    (t : RBTree.RBNode.Stream α) →
      ((t : RBTree.RBNode.Stream α) → RBTree.RBNode.Stream.below t → motive t) →
        motive t ×' RBTree.RBNode.Stream.below t
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A continuous function whose support is contained in a compact set is strongly measurable.  -/
Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : One β] {f : α → β},
  Continuous f → ∀ {k : Set α}, IsCompact k → Function.mulSupport f ⊆ k → MeasureTheory.StronglyMeasurable f
-- Mathlib.Analysis.Normed.Group.Constructions
Additive.seminormedAddGroup : {E : Type u_2} → [SeminormedGroup E] → SeminormedAddGroup (Additive E)
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- `saturation` forms a `GaloisInsertion` with the forgetful functor
`SaturatedAddSubmonoid.toAddSubmonoid`.  -/
AddSubmonoid.giSaturation : (M : Type u_1) → [inst : AddZeroClass M] → GaloisInsertion AddSubmonoid.saturation fun x => x.toAddSubmonoid
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_self : ∀ (a b : ℤ), b * a.fdiv b = a - a.fmod b
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_sdiff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (s t : TopologicalSpace.CompactOpens α),
  ↑(s \ t) = ↑s \ ↑t
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj F).hom.app X =
    CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X).1)
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.mk : ∀ {k : Type u} [inst : Field k], (∀ (p : Polynomial k), p.Separable → p.Splits) → IsSepClosed k
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.ofAdd_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Multiplicative.ofAdd a ≤ Multiplicative.ofAdd b ↔ a ≤ b
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.image_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (f : F ⟶ F'),
  ⊤.image f = CategoryTheory.Subfunctor.range f
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.val_neg : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (x : ↥s), ↑(-x) = -↑x
-- ProofWidgets.Util
instMonadSaveCtxStateRefT'OfMonadLiftTST : {m n : Type → Type} →
  [Monad m] → [MonadSaveCtx m n] → {ω σ : Type} → [MonadLiftT (ST ω) m] → MonadSaveCtx (StateRefT' ω σ m) n
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I}
  (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a)
  (hk :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b))
  (a : J.L) {Z : C} (h : I.left a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk)
      (CategoryTheory.CategoryStruct.comp (K.ι a) h) =
    CategoryTheory.CategoryStruct.comp (k a) h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], (t₁ \ t₂)[k]! = if k ∈ t₂ then default else t₁[k]!
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInfTopHom.eq_1 : ExpGrowth.expGrowthInfTopHom =
  { toFun := ExpGrowth.expGrowthInf, map_inf' := ⋯, map_top' := ExpGrowth.expGrowthInf_top }
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearCombination_repr : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v) (x : ↥(Submodule.span R (Set.range v))),
  (Finsupp.linearCombination R v) (hv.repr x) = ↑x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_restrictVar : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : DecidableEq α]
  {t : L.Term α} {f : ↥t.varFinset → β} {v : β → M} (v' : α → M),
  (∀ (a : ↥t.varFinset), v (f a) = v' ↑a) →
    FirstOrder.Language.Term.realize v (t.restrictVar f) = FirstOrder.Language.Term.realize v' t
-- Mathlib.Algebra.Module.LinearMap.End
/-- When `f` is an `R`-linear map taking values in `S`, then `fun b ↦ f b • x` is an `R`-linear
map.  -/
LinearMap.smulRight : {R : Type u_1} →
  {S : Type u_3} →
    {M : Type u_4} →
      {M₁ : Type u_5} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Semiring S] →
                    [inst_6 : Module R S] →
                      [inst_7 : Module S M] → [IsScalarTower R S M] → (M₁ →ₗ[R] S) → M → M₁ →ₗ[R] M
-- Mathlib.Computability.RegularExpressions
RegularExpression.instOne : {α : Type u_1} → One (RegularExpression α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_right_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C), (X.homologyData₀ R).right.H = ∐ fun x => R
-- Mathlib.RingTheory.RingHom.Flat
/-- If `S ⊗[R] S → S` is flat, then also `T ⊗[R] A → T ⊗[S] A` is flat.  -/
RingHom.Flat.mapOfCompatibleSMul : ∀ {R S : Type u} (T A : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : CommRing A]
  [inst_4 : Algebra R S] [inst_5 : Algebra R T] [inst_6 : Algebra S T] [inst_7 : IsScalarTower R S T]
  [inst_8 : Algebra R A] [inst_9 : Algebra S A] [inst_10 : IsScalarTower R S A],
  (Algebra.TensorProduct.lmul' R).Flat → (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).Flat
-- Init.Data.Rat.Lemmas
Rat.sub_lt_iff : ∀ {a b c : ℚ}, a - c < b ↔ a < b + c
-- Mathlib.Data.Sym.Basic
Sym.ofVector_nil : ∀ {α : Type u_1}, Sym.ofVector List.Vector.nil = Sym.nil
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_eq_singleton_iff_isBot : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α}, Set.Iic x = {x} ↔ IsBot x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) = true},
  (m₁.inter m₂ ⋯).get k h_contains = m₁.get k ⋯
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.rightToLeft.eq_1 : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful],
  t.rightToLeft =
    ((CategoryTheory.Functor.FullyFaithful.ofFullyFaithful G).whiskeringRight C).preimage
      (CategoryTheory.CategoryStruct.comp t.adj₂.counit t.adj₁.unit)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {fallback : β a},
  Std.Internal.List.getValueCastD a (Std.Internal.List.insertEntryIfNew k v l) fallback =
    if h : (k == a) = true ∧ Std.Internal.List.containsKey k l = false then cast ⋯ v
    else Std.Internal.List.getValueCastD a l fallback