mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk.inj : ∀ {M : Type u_3} {inst : AddZeroClass M} {toAddSubsemigroup : AddSubsemigroup M}
  {zero_mem' : 0 ∈ toAddSubsemigroup.carrier} {toAddSubsemigroup_1 : AddSubsemigroup M}
  {zero_mem'_1 : 0 ∈ toAddSubsemigroup_1.carrier},
  { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' } =
      { toAddSubsemigroup := toAddSubsemigroup_1, zero_mem' := zero_mem'_1 } →
    toAddSubsemigroup = toAddSubsemigroup_1
-- Mathlib.GroupTheory.Congruence.Defs
/-- Two congruence relations are equal iff their underlying binary relations are equal.  -/
Con.coe_inj : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, ⇑c = ⇑d ↔ c = d
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_def : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : Multiplicative M →* A),
  ⇑((AddMonoidAlgebra.lift R A M) F) = ⇑(AddMonoidAlgebra.liftNC ↑(algebraMap R A) ⇑F)
-- Init.Data.SInt.Lemmas
Int8.toBitVec_toInt32 : ∀ (x : Int8), x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `f : X → Y` is `K`-Lipschitz on `s`, then `μH[d] (f '' s) ≤ K ^ d * μH[d] s`.  -/
LipschitzOnWith.hausdorffMeasure_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {K : NNReal} {f : X → Y} {s : Set X},
  LipschitzOnWith K f s →
    ∀ {d : ℝ},
      0 ≤ d →
        (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The kernel of `quotLeftToQuotSup`  -/
DoubleQuot.ker_quotLeftToQuotSup : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R),
  RingHom.ker (DoubleQuot.quotLeftToQuotSup I J) = Ideal.map (Ideal.Quotient.mk I) J
-- Mathlib.Algebra.Quaternion
Quaternion.instIsDomain : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R], IsDomain (Quaternion R)
-- Init.Data.Vector.Attach
Vector.pmap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a),
  Vector.pmap (fun a x => f a) xs H = Vector.map f xs
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_iff_strictAnti_get`. -/
StrictAnti.sortedGT : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], StrictAnti l.get → l.SortedGT
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.postcomp_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {T : Type w₂} (φ : c.pt → T), (c.postcomp φ).pt = T
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.unop.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N], MonoidHom.unop = MonoidHom.op.symm
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type uE) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] (i : ι), ContDiff 𝕜 n fun f => f i
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset_2 : HAdd Std.Time.DateTime Std.Time.Hour.Offset Std.Time.DateTime
-- Mathlib.RingTheory.FormalGroup.Basic
/-- The coefficient of $Y$ in $F(X, Y)$ is 1.  -/
FormalGroup.lin_coeff_Y : ∀ {R : Type u_1} [inst : CommRing R] (self : FormalGroup R), (MvPowerSeries.coeff fun₀ | 1 => 1) self.toPowerSeries = 1
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A domain that is module-finite as an algebra over a field is a division ring.  -/
divisionRingOfFiniteDimensional : (F : Type u_1) →
  (K : Type u_2) →
    [inst : Field F] →
      [inst_1 : Ring K] → [IsDomain K] → [inst_3 : Algebra F K] → [FiniteDimensional F K] → DivisionRing K
-- Init.NotationExtra
unexpandExists : Lean.PrettyPrinter.Unexpander
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_pos : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {p : Prop} {f : p → α} (hp : p), ⨅ (h : p), f h = f hp
-- Mathlib.Probability.Decision.Risk.Basic
/-- For a bounded loss, the Bayes risk with respect to a prior is bounded by a constant.
See `bayesRisk_le_mul` for the usual cases where all measures are probability measures.  -/
ProbabilityTheory.bayesRisk_le_mul' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [h𝓨 : Nonempty 𝓨] (P : ProbabilityTheory.Kernel Θ 𝓧)
  (π : MeasureTheory.Measure Θ) {C : NNReal},
  (∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C) → ProbabilityTheory.bayesRisk ℓ P π ≤ ↑C * P.bound * π Set.univ
-- Init.Grind.Norm
Lean.Grind.cond_eq_ite : ∀ {α : Sort u_1} (c : Bool) (a b : α), (bif c then a else b) = if c = true then a else b
-- Lean.ToExpr
Lean.instToExprBool : Lean.ToExpr Bool
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.basis_repr_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {V : Type u_3}
  [inst_3 : AddCommMonoid V] [inst_4 : Module R V] {W : Type u_4} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module S W] [inst_8 : IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V)
  (ibc : IsBaseChange S ε) (v : V),
  (IsBaseChange.basis b ibc).repr (ε v) = (Finsupp.mapRange.linearMap (Algebra.linearMap R S)) (b.repr v)
-- Lean.Data.Lsp.Basic
Lean.Lsp.SnippetString.value : Lean.Lsp.SnippetString → String
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Set.mk_mem_sym2_iff`. -/
Set.mk'_mem_sym2_iff : ∀ {α : Type u_1} {s : Set α} {x y : α}, s(x, y) ∈ s.sym2 ↔ x ∈ s ∧ y ∈ s
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- The entries of a Gram matrix are inner products of vectors in an inner product space.  -/
Matrix.gram : {E : Type u_1} → {n : Type u_2} → (𝕜 : Type u_5) → [Inner 𝕜 E] → (n → E) → Matrix n n 𝕜
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertIfNew!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.insertIfNew! k v t =
    if Std.DTreeMap.Internal.Impl.contains k t = true then t else Std.DTreeMap.Internal.Impl.insert! k v t
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- This is the map on the cotangent space associated to a map of presentation.
The matrix associated to this map is the Jacobian matrix. See `CotangentSpace.repr_map`.
 -/
Algebra.Extension.CotangentSpace.map : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u'} →
              {S' : Type v'} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] →
                              [IsScalarTower R R' S'] → P.Hom P' → P.CotangentSpace →ₗ[S] P'.CotangentSpace
-- Mathlib.Data.ENNReal.Basic
ENNReal.instDistribLattice : DistribLattice ENNReal
-- Init.Data.List.Lemmas
List.getElem_zero_eq_head : ∀ {α : Type u_1} {l : List α} (h : 0 < l.length), l[0] = l.head ⋯
-- Mathlib.NumberTheory.ModularForms.LFunction
CuspForm.differentiable_L : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : CuspFormClass F Γ k], Differentiable ℂ (ModularForm.L hk f)
-- Mathlib.MeasureTheory.Measure.Tight
MeasureTheory.IsTightMeasureSet.map : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [inst : TopologicalSpace 𝓧]
  [inst_1 : TopologicalSpace 𝓨] [inst_2 : MeasurableSpace 𝓨] [OpensMeasurableSpace 𝓨] [T2Space 𝓨],
  MeasureTheory.IsTightMeasureSet S →
    ∀ {f : 𝓧 → 𝓨}, Continuous f → MeasureTheory.IsTightMeasureSet (MeasureTheory.Measure.map f '' S)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.mulEquivPiModRangePowMonoidHom_apply : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : (i : ι) → CommGroup (A i)] (n : ℕ) (x : (i : ι) → A i),
  (QuotientGroup.mulEquivPiModRangePowMonoidHom A n) ↑x = fun i => ↑(x i)
-- Lean.Widget.Types
Lean.Widget.WidgetInstance.mk : Lean.Name → UInt64 → StateM Lean.Server.RpcObjectStore Lean.Json → Lean.Widget.WidgetInstance
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ne_zero_of_unit : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀]
  (v : Valuation K Γ₀) (x : Kˣ), v ↑x ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_inv_two_im_eq_sqrt : ∀ {x : ℂ}, 0 ≤ x.im → (x ^ 2⁻¹).im = √((‖x‖ - x.re) / 2)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_of_integral_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → ∫ (x : Ω), X x ∂μ = 0 → ProbabilityTheory.variance X μ = ∫ (ω : Ω), X ω ^ 2 ∂μ
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous iff `range 𝓕` is equicontinuous,
i.e the family `(↑) : range F → X → α` is equicontinuous.  -/
equicontinuous_iff_range : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
  Equicontinuous F ↔ Equicontinuous Subtype.val
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)}
  {hc : k' ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.get k' hc =
    if heq : compare k k' = Ordering.eq then cast ⋯ ((f (t.get? k)).get ⋯) else t.get k' ⋯
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_one : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Ioc_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.Ioc (Fin.natAdd m i) (Fin.natAdd m j) = Set.Ioc i j
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y)
  (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) (c : (SimplexCategory.Truncated n)ᵒᵖ),
  (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
-- Mathlib.Topology.Algebra.Star
/-- The star operation bundled as a continuous map.  -/
starContinuousMap : {R : Type u_2} → [inst : TopologicalSpace R] → [inst_1 : Star R] → [ContinuousStar R] → C(R, R)
-- Init.Omega.Constraint
Lean.Omega.Constraint.mk.sizeOf_spec : ∀ (lowerBound : Lean.Omega.LowerBound) (upperBound : Lean.Omega.UpperBound),
  sizeOf { lowerBound := lowerBound, upperBound := upperBound } = 1 + sizeOf lowerBound + sizeOf upperBound
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.biproductIsoPi_inv_comp_π : ∀ {R : Type u} [inst : Ring R] {J : Type} [inst_1 : Finite J] (f : J → ModuleCat R) (j : J),
  CategoryTheory.CategoryStruct.comp (ModuleCat.biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) =
    ModuleCat.ofHom (LinearMap.proj j)
-- Mathlib.GroupTheory.OrderOfElement
vadd_eq_self_of_mem_zmultiples : ∀ {G : Type u_6} [inst : AddGroup G] {x y : G} {α : Type u_7} [inst_1 : AddAction G α],
  x ∈ AddSubgroup.zmultiples y → ∀ {a : α}, y +ᵥ a = a → x +ᵥ a = a
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The natural inclusion from the functor induced by a sieve to the yoneda embedding.  -/
CategoryTheory.Sieve.functorInclusion : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Sieve X) → S.functor ⟶ CategoryTheory.yoneda.obj X
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprPasswdInfo.repr : Std.Internal.UV.System.PasswdInfo → ℕ → Std.Format
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (β : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk sq₁₃.π),
  CategoryTheory.CategoryStruct.comp sq₁₂.inr (CategoryTheory.Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) =
    adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right β) sq₁₃.fst)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.id_obj : ∀ (X : CategoryTheory.ReflQuiv) (x : ↑X), (CategoryTheory.CategoryStruct.id X).obj x = x
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Any morphism `Z ⟶ X⟦1⟧` is part of a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧`  -/
CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] {Z X : C}
  (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  ∃ Y f g, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.Group.Semiconj.Basic
/-- **Alias** of the reverse direction of `AddSemiconjBy.neg_symm_left_iff`. -/
AddSemiconjBy.neg_symm_left : ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy (-a) y x
-- Mathlib.Data.List.Basic
List.foldl_fixed' : ∀ {α : Type u} {β : Type v} {f : α → β → α} {a : α}, (∀ (b : β), f a b = a) → ∀ (l : List β), List.foldl f a l = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.get_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} (hk : k ∈ t₁),
  t₁.get k hk = t₂.get k ⋯
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.prefix.injEq : ∀ (s s_1 : Lean.Grind.AC.Seq), (Lean.Grind.AC.SubseqResult.prefix s = Lean.Grind.AC.SubseqResult.prefix s_1) = (s = s_1)
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.mk.injEq : ∀ (method : Aesop.ScriptGenerated.Method) (perfect hasMVar : Bool) (method_1 : Aesop.ScriptGenerated.Method)
  (perfect_1 hasMVar_1 : Bool),
  ({ method := method, perfect := perfect, hasMVar := hasMVar } =
      { method := method_1, perfect := perfect_1, hasMVar := hasMVar_1 }) =
    (method = method_1 ∧ perfect = perfect_1 ∧ hasMVar = hasMVar_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  W.Ψ n = Polynomial.C (W.preΨ n) * if Even n then W.ψ₂ else 1
-- Mathlib.Data.Matrix.Basic
/-- A version of `Set.matrix` for `Subsemiring`s.
Given a `Subsemiring` `S`, `S.matrix` is the `Subsemiring` of square matrices `m`
all of whose entries `m i j` belong to `S`.  -/
Subsemiring.matrix : {n : Type u_3} →
  {R : Type u_14} →
    [inst : NonAssocSemiring R] →
      [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → Subsemiring R → Subsemiring (Matrix n n R)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.rat_add_iff : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function which is continuous on a compact set `s` is almost everywhere strongly measurable
with respect to `μ.restrict t` for any measurable subset `t` of `s`.  -/
ContinuousOn.aestronglyMeasurable_of_subset_isCompact : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_2 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {s t : Set α}
  {μ : MeasureTheory.Measure α},
  ContinuousOn f s → IsCompact s → MeasurableSet t → t ⊆ s → MeasureTheory.AEStronglyMeasurable f (μ.restrict t)
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsImmersion g],
  AlgebraicGeometry.IsImmersion (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsImmersion f
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_prod : ∀ {β : Type u_3} {M : Type u_5} {α : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] (c : M) (s : Set α) (t : Set β),
  c +ᵥ s ×ˢ t = (c +ᵥ s) ×ˢ (c +ᵥ t)
-- Init.Data.List.Count
List.countP_replicate : ∀ {α : Type u_1} {p : α → Bool} {a : α} {n : ℕ}, List.countP p (List.replicate n a) = if p a = true then n else 0
-- Lean.Server.References
/-- Converts `i` to a JSON-serializable `Lsp.RefInfo` and collects its decls.  -/
Lean.Server.RefInfo.toLspRefInfo : Lean.Server.RefInfo → StateT Lean.Lsp.Decls BaseIO Lean.Lsp.RefInfo
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The right action of a map `f : c ⟶ c'` in `C` on an object `d` in `D`.
If we are to consider the action as a functor `Α : C ⥤ D ⥤ D`,
this is `(Α.map f).app d`. This is denoted `d ⊴ᵣ f`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight : {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.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            (d : D) →
              {c c' : C} →
                (c ⟶ c') →
                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶
                    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c')
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.sectionsEquivHom_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G)
  (X : Type u₂) [inst_1 : Unique X] (x : ↑F.sections),
  (G.sectionsEquivHom X) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f)) x) =
    CategoryTheory.CategoryStruct.comp ((F.sectionsEquivHom X) x) f
-- Mathlib.Data.Int.Log
Int.clog_of_right_le_one : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) {r : R}, r ≤ 1 → Int.clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
-- Lean.Language.Basic
Lean.Language.SnapshotTree.mk : Lean.Language.Snapshot → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than the given key.
 -/
Std.ExtDTreeMap.getEntryGT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → (a : α) × β a
-- Mathlib.Data.Sum.Order
OrderIso.sumLexEmpty_apply_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] [inst_2 : IsEmpty β] (x : α),
  OrderIso.sumLexEmpty (toLex (Sum.inl x)) = x
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.t0Space : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [T0Space F] (b : B), T0Space (E b)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ioc : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] (a b : R),
  f.measure (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.size_eq_if_roc : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.size = if r.lower ≤ r.upper then (r.lower<...=r.upper).size + 1 else 0
-- Mathlib.Topology.Category.Compactum
/-- A local definition used only in the proofs.  -/
_private.Mathlib.Topology.Category.Compactum.0.Compactum.basic : {X : Compactum} → Set X.A → Set (Ultrafilter X.A)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  (ContDiffMapSupportedIn.toBoundedContinuousFunctionLM 𝕜) f = { toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower'_repr : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (ij : ι' × ι),
  ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2
-- Mathlib.Topology.Bases
/-- The image of a topological basis "downstairs" in an open quotient is a topological basis.  -/
TopologicalSpace.IsTopologicalBasis.quotient : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Setoid X} {V : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis V →
    IsOpenMap Quotient.mk' → TopologicalSpace.IsTopologicalBasis (Set.image Quotient.mk' '' V)
-- Mathlib.Order.BooleanGenerators
/-- A compactly generated complete lattice generated by Boolean generators is a Boolean algebra.  -/
IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop : {α : Type u_1} →
  [inst : CompleteLattice α] →
    {S : Set α} → [IsCompactlyGenerated α] → IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → BooleanAlgebra α
-- Lean.LocalContext
Lean.LocalContext.find? : Lean.LocalContext → Lean.FVarId → Option Lean.LocalDecl
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- An induction principle for additive closure membership. If
`p` holds for all elements of `s`, and is preserved under addition, then `p` holds for all
elements of the additive closure of `s`.  -/
AddSubsemigroup.closure_induction : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop},
  (∀ (x : M) (h : x ∈ s), p x ⋯) →
    (∀ (x y : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s),
        p x hx → p y hy → p (x + y) ⋯) →
      ∀ {x : M} (hx : x ∈ AddSubsemigroup.closure s), p x hx
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.denote : Nat.Internal.Linear.Context → Nat.Internal.Linear.ExprCnstr → Prop
-- Mathlib.Analysis.Normed.Field.Lemmas
DilationEquiv.mulLeft_symm_apply : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α),
  (DilationEquiv.mulLeft a ha).symm x = a⁻¹ * x