mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.inclusion_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T U : NonUnitalSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S),
  (NonUnitalSubalgebra.inclusion htu) ((NonUnitalSubalgebra.inclusion hst) x) = (NonUnitalSubalgebra.inclusion ⋯) x
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.eventually_notMem_thickening_of_infEDist_pos`.

---

An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
(open) `δ`-thickening of `E` for small enough positive `δ`.  -/
Metric.eventually_notMem_thickening_of_infEdist_pos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {E : Set α} {x : α},
  x ∉ closure E → ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.thickening δ E
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_one_div : ∀ {a b : ℝ}, 0 ∉ Set.uIcc a b → ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
-- Init.Data.Int.DivMod.Lemmas
Int.sub_bmod_bmod : ∀ {x y : ℤ} {n : ℕ}, (x - y.bmod n).bmod n = (x - y).bmod n
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prime_pow_dvd_iff_le : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {m p : Associates α},
  m ≠ 0 → Irreducible p → ∀ {k : ℕ}, p ^ k ≤ m ↔ k ≤ p.count m.factors
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.evalObtain : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.comp_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- (Implementation detail): A small skeleton of `FGAlgCat`.  -/
FGAlgCatSkeleton : (R : Type u) → [CommRing R] → Type u
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.map_nonsingular : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (x y : R), (W.map f).Nonsingular (f x) (f y) ↔ W.Nonsingular x y
-- Mathlib.Probability.Kernel.Posterior
/-- The posterior is a Markov kernel.  -/
ProbabilityTheory.instIsMarkovKernelPosterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω],
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.posterior κ μ)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH2_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.shortComplexH2 A).f = groupHomology.d₃₂ A
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.mk.injEq : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.ExtTreeMap._auto_1}
  (inner inner_1 : Std.ExtDTreeMap α (fun x => β) cmp), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.Cochain₀.mul_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C) (γ₁ γ₂ : CategoryTheory.PresheafOfGroups.ZeroCochain G U) (i : I), (γ₁ * γ₂) i = γ₁ i * γ₂ i
-- Mathlib.Algebra.Algebra.Opposite
DistribSMul.toLinearMap.congr_simp : ∀ (R : Type u_1) {S : Type u_3} (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DistribSMul S M] [inst_4 : SMulCommClass S R M] (s s_1 : S),
  s = s_1 → DistribSMul.toLinearMap R M s = DistribSMul.toLinearMap R M s_1
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.monotone_iUnionUpTo : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α),
  Monotone p.iUnionUpTo
-- Init.Tactics
/-- `unhygienic tacs` runs `tacs` with name hygiene disabled.
This means that tactics that would normally create inaccessible names will instead
make regular variables. **Warning**: Tactics may change their variable naming
strategies at any time, so code that depends on autogenerated names is brittle.
Users should try not to use `unhygienic` if possible.
```
example : ∀ x : Nat, x = x := by unhygienic
  intro            -- x would normally be intro'd as inaccessible
  exact Eq.refl x  -- refer to x
```
 -/
Lean.Parser.Tactic.tacticUnhygienic_ : Lean.ParserDescr
-- Init.Data.Bool
Bool.instDecidableLt : (x y : Bool) → Decidable (x < y)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.mk : Bool → Bool → Bool → BoxIntegral.IntegrationParams
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingCompOf_le_posFittingComp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (x : L), LieModule.posFittingCompOf R M x ≤ LieModule.posFittingComp R L M
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.eqToHom_apply : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β : Type w} {X Y : β → C} (h : X = Y) (b : β),
  CategoryTheory.eqToHom h b = CategoryTheory.eqToHom ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β k}, ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v
-- Mathlib.Logic.Unique
unique_iff_subsingleton_and_nonempty : ∀ (α : Sort u), Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- `CategoryStruct` on `B ⥤ᴸ C` where the (1-)morphisms are given by oplax
transformations.  -/
CategoryTheory.Lax.OplaxTrans.instCategoryStructLaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.LaxFunctor B C)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.getKey!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getKey! k = m₂.getKey! k
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.mk.sizeOf_spec : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
  (δ_castSucc_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam)
  (δ_succ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam)
  (δ_succ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam)
  (δ_map_of_lt :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam),
  sizeOf
      { map := map, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map, δ_succ_castSucc_map := δ_succ_castSucc_map,
        δ_succ_succ_map := δ_succ_succ_map, δ_map_of_lt := δ_map_of_lt, δ_map_of_gt := δ_map_of_gt } =
    1 + sizeOf map + sizeOf δ_castSucc_castSucc_map + sizeOf δ_succ_castSucc_map + sizeOf δ_succ_succ_map
-- Init.Prelude
/-- The notation typeclass for inverses.
This enables the notation `a⁻¹ : α` where `a : α`.
 -/
Inv : Type u → Type u
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_neg : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i), lp.single p i (-a) = -lp.single p i a
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_associator_inv : ∀ {B : Type u} [inst : Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h) =
    (CategoryTheory.Bicategory.associator f g h).inv
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.inv_zpow' : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), A⁻¹ ^ n = A ^ (-n)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_ofNat : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) (n : ℕ) [inst_3 : n.AtLeastTwo], (MvPolynomial.aeval f) (OfNat.ofNat n) = OfNat.ofNat n
-- Init.Data.Float.Model.Float
/-- Converts an `Int32` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofInt32 : Int32 → Float.Model
-- Mathlib.Analysis.SpecificLimits.Basic
summable_geometric_two : Summable fun n => (1 / 2) ^ n
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrRight_apply : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [hp : Fact (1 ≤ p)]
  [inst : Fintype ι] [inst_1 : Semiring 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_4 : (i : ι) → Module 𝕜 (α i)]
  [inst_5 : (i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i) (x : PiLp p α),
  (LinearIsometryEquiv.piLpCongrRight p e) x = WithLp.toLp p fun i => (e i) (x.ofLp i)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (k : K) (f : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.peek k f q, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_2 k f q v S
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.map_natDegree_eq_natDegree : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} {F : Type u_3} [inst_1 : Semiring S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F}
  (p : Polynomial R),
  (∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n) → (φ p).natDegree = p.natDegree
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.analyticAt : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f p x → AnalyticAt 𝕜 f x
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIocMod.congr_simp : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), QuotientAddGroup.equivIocMod hp a = QuotientAddGroup.equivIocMod hp a
-- Mathlib.Order.CompleteBooleanAlgebra
Prod.instCompletelyDistribLattice : {α : Type u} →
  {β : Type v} → [CompletelyDistribLattice α] → [CompletelyDistribLattice β] → CompletelyDistribLattice (α × β)
-- Aesop.Rule.Name
Aesop.instHashableBuilderName.hash : Aesop.BuilderName → UInt64
-- Mathlib.Order.CompleteLattice.Defs
ofDual_sSup : ∀ {α : Type u_1} [inst : InfSet α] (s : Set αᵒᵈ), OrderDual.ofDual (sSup s) = sInf (⇑OrderDual.toDual ⁻¹' s)
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain_apply_image : ∀ {α' : Type u_9} {β' : Type u_10} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  (a : α'), (e.extendDomain f) ↑(f a) = ↑(f (e a))
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.get?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.get?ₘ a = Std.DHashMap.Internal.AssocList.getCast? a (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a)
-- Mathlib.Order.CompleteLatticeIntervals
Set.Icc.coe_sInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set ↑(Set.Icc a b)},
  S.Nonempty →
    have this := ⋯;
    ↑(sInf S) = sInf (Subtype.val '' S)
-- Mathlib.Order.Filter.EventuallyConst
/-- **Alias** of the forward direction of `Filter.eventuallyConst_iff_tendsto`. -/
Filter.EventuallyConst.exists_tendsto : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β],
  Filter.EventuallyConst f l → ∃ x, Filter.Tendsto f l (pure x)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSum.match_1.eq_1 : ∀ {n m : ℕ} (motive : Fin n ⊕ Fin m → Sort u_1) (x : Fin n) (h_1 : (x : Fin n) → motive (Sum.inl x))
  (h_2 : (x : Fin m) → motive (Sum.inr x)),
  (match Sum.inl x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_1 x
-- Batteries.Control.AlternativeMonad
StateRefT'.instLawfulAlternativeLift : ∀ {m : Type → Type} {ω σ : Type} [inst : AlternativeMonad m], LawfulAlternativeLift m (StateRefT' ω σ m)
-- Mathlib.Topology.Algebra.Semigroup
/-- A version of
`exists_idempotent_of_compact_t2_of_continuous_add_left` where the idempotent lies in
some specified nonempty compact additive subsemigroup.  -/
exists_idempotent_in_compact_add_subsemigroup : ∀ {M : Type u_1} [inst : AddSemigroup M] [inst_1 : TopologicalSpace M] [T2Space M],
  (∀ (r : M), Continuous fun x => x + r) →
    ∀ (s : Set M), s.Nonempty → IsCompact s → (∀ x ∈ s, ∀ y ∈ s, x + y ∈ s) → ∃ m ∈ s, m + m = m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_union!_le_size_add_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → (m₁.union! m₂).size ≤ m₁.size + m₂.size
-- Mathlib.Algebra.Order.Group.PosPart
div_mabs_eq_inv_leOnePart_sq : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a : α), a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support is bounded above.  -/
Continuous.bddAbove_range_of_hasCompactSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] [inst_4 : Zero α] {f : β → α}, Continuous f → HasCompactSupport f → BddAbove (Set.range f)
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.mulActionBaseChange_smul_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (a : A) (s : S) (x : Ω[A⁄R]), a • s ⊗ₜ[R] x = s ⊗ₜ[R] (a • x)
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.mk.sizeOf_spec : ∀ (isHoverPosOnStop : Bool) (size : ℕ) (isVariableInfo isPartialTermInfo : Bool),
  sizeOf
      { isHoverPosOnStop := isHoverPosOnStop, size := size, isVariableInfo := isVariableInfo,
        isPartialTermInfo := isPartialTermInfo } =
    1 + sizeOf isHoverPosOnStop + sizeOf size + sizeOf isVariableInfo + sizeOf isPartialTermInfo
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_ofDual : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α] (a b : αᵒᵈ),
  (IncidenceAlgebra.mu 𝕜) (OrderDual.ofDual a) (OrderDual.ofDual b) = (IncidenceAlgebra.mu 𝕜) b a
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The isomorphism between `(lift F _ _).obj WithTerminal.star` with `Z`.  -/
CategoryTheory.WithTerminal.liftStar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → F.obj x ⟶ Z) →
              (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) →
                (CategoryTheory.WithTerminal.lift F M hM).obj CategoryTheory.WithTerminal.star ≅ Z
-- Lean.Expr
/-- Given `a b : Int`, returns `a ^ b`  -/
Lean.mkIntPowNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.eval_πs_image : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I]
  {l : Profinite.NobelingProof.Products I} {o : Ordinal.{u}},
  (∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o) →
    Profinite.NobelingProof.Products.eval C '' {m | m < l} =
      ⇑(Profinite.NobelingProof.πs C o) ''
        Profinite.NobelingProof.Products.eval
            (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ''
          {m | m < l}
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of `continuousWithinAt_iff_continuousAt_domRestrict`. -/
continuousWithinAt_iff_continuousAt_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {x : α}
  {s : Set α} (h : x ∈ s), ContinuousWithinAt f s x ↔ ContinuousAt (s.domRestrict f) ⟨x, h⟩
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- If `R` is an `S`-algebra, a root pairing over `R` is said to be valued in `S` if the pairing
between a root and coroot always belongs to `S`.

Of particular interest is the case `S = ℤ`. See `RootPairing.IsCrystallographic`.  -/
RootPairing.IsValuedIn : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  RootPairing ι R M N → (S : Type u_6) → [inst_5 : CommRing S] → [Algebra S R] → Prop
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductFunctor_obj_map : ∀ (X : Type u) {x Y₂ : Type u} (f : x ⟶ Y₂),
  (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).map f =
    (CategoryTheory.Limits.Types.binaryProductLimit X Y₂).lift
      (CategoryTheory.Limits.BinaryFan.mk (TypeCat.ofHom Prod.fst)
        (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom Prod.snd) f))
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.coe_snoc : ∀ {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ Set.range ⇑x), ⇑(Fin.Embedding.snoc x ha) = Fin.snoc (⇑x) a
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.isLeftUniformGroup : ∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], IsLeftUniformGroup α
-- Mathlib.Order.Minimal
MinimalFor.maximalFor_of_strictAntiOn_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {Q : ι → Prop} {f : ι → α}
  {g : α → β} {i : ι}, StrictAntiOn g (f '' Set.ofPred Q) → MinimalFor Q (g ∘ f) i → MaximalFor Q f i
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.map_rootsOfUnity : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [inst_2 : CommRing S] [IsDomain S]
  [inst_4 : FunLike F R S] [inst_5 : MonoidHomClass F R S] {ζ : R} {n : ℕ} [NeZero n],
  IsPrimitiveRoot ζ n →
    ∀ {f : F}, Function.Injective ⇑f → Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_union_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α} (h : m₂.contains k = true),
  Std.DHashMap.Internal.Raw₀.Const.get (m₁.union m₂) k ⋯ = Std.DHashMap.Internal.Raw₀.Const.get m₂ k h
-- Mathlib.LinearAlgebra.QuadraticForm.Real
/-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted
sum of squares with the weights being ±1, `SignType` version.  -/
QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q) →
    ∃ w,
      (∀ (i : Fin (Module.finrank ℝ M)), w i ≠ 0) ∧
        QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))
-- Init.Data.SInt.Basic
/-- The power operation, raising a 16-bit signed integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
Int16.pow : Int16 → ℕ → Int16
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Icc_of_Ioo : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Ioo (a i) (b i)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.iterate_bijective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M}, Function.Bijective ⇑f' → ∀ (n : ℕ), Function.Bijective ⇑(f' ^ n)
-- Init.Data.Char.Ordinal
Char.succMany?_eq : ∀ {m : ℕ} {c : Char}, Char.succMany? m c = Option.map Char.ofOrdinal (c.ordinal.addNat? m)
-- Mathlib.Analysis.Complex.Norm
Complex.lim_norm : ∀ (f : CauSeq ℂ fun x => ‖x‖), (Complex.cauSeqNorm f).lim = ‖f.lim‖
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hom_inv_apply : ∀ {X Y : BoolAlg} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s