mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.mk.hcongr_15 : ∀ (R R' : Type u_1),
  R = R' →
    ∀ (A A' : Type u_2),
      A = A' →
        ∀ (inst : CommRing R) (inst' : CommRing R'),
          inst ≍ inst' →
            ∀ (inst_1 : Ring A) (inst'_1 : Ring A'),
              inst_1 ≍ inst'_1 →
                ∀ (inst_2 : Algebra R A) (inst'_2 : Algebra R' A'),
                  inst_2 ≍ inst'_2 →
                    ∀ (c₁ : R) (c₁' : R'),
                      c₁ ≍ c₁' →
                        ∀ (c₂ : R) (c₂' : R'),
                          c₂ ≍ c₂' →
                            ∀ (c₃ : R) (c₃' : R'),
                              c₃ ≍ c₃' →
                                ∀ (i : A) (i' : A'),
                                  i ≍ i' →
                                    ∀ (j : A) (j' : A'),
                                      j ≍ j' →
                                        ∀ (k : A) (k' : A'),
                                          k ≍ k' →
                                            ∀ (i_mul_i : i * i = c₁ • 1 + c₂ • i)
                                              (i_mul_i' : i' * i' = c₁' • 1 + c₂' • i'),
                                              i_mul_i ≍ i_mul_i' →
                                                ∀ (j_mul_j : j * j = c₃ • 1) (j_mul_j' : j' * j' = c₃' • 1),
                                                  j_mul_j ≍ j_mul_j' →
                                                    ∀ (i_mul_j : i * j = k) (i_mul_j' : i' * j' = k'),
                                                      i_mul_j ≍ i_mul_j' →
                                                        ∀ (j_mul_i : j * i = c₂ • j - k)
                                                          (j_mul_i' : j' * i' = c₂' • j' - k'),
                                                          j_mul_i ≍ j_mul_i' →
                                                            { i := i, j := j, k := k, i_mul_i := i_mul_i,
                                                                j_mul_j := j_mul_j, i_mul_j := i_mul_j,
                                                                j_mul_i := j_mul_i } ≍
                                                              { i := i', j := j', k := k', i_mul_i := i_mul_i',
                                                                j_mul_j := j_mul_j', i_mul_j := i_mul_j',
                                                                j_mul_i := j_mul_i' }
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- If a function has compact support, then either the function is trivial
or the space is finite-dimensional.  -/
HasCompactSupport.eq_zero_or_finiteDimensional : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_5} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  {X : Type u_7} [inst_8 : TopologicalSpace X] [inst_9 : Zero X] [T1Space X] {f : E → X},
  HasCompactSupport f → Continuous f → f = 0 ∨ FiniteDimensional 𝕜 E
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Expressing uniform convergence on a set using `dist`.  -/
Metric.tendstoUniformlyOn_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_1} [inst : PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι}
  {s : Set β}, TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap e.inv (e.hom x))
      (AlgebraicGeometry.Scheme.Hom.stalkMap e.hom x) =
    (X.presheaf.stalkCongr ⋯).hom
-- Mathlib.Data.Nat.Factorial.Basic
/-- `Nat.factorial n` is the factorial of `n`.  -/
Nat.factorial : ℕ → ℕ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_div'' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b c d : α},
  a < b → c < d → a / d < b / c
-- Mathlib.Analysis.Normed.Ring.Basic
SubringClass.toNormedCommRing : {S : Type u_5} →
  {R : Type u_6} → [inst : SetLike S R] → [inst_1 : NormedCommRing R] → [SubringClass S R] → (s : S) → NormedCommRing ↥s
-- Mathlib.CategoryTheory.Shift.Induced
/-- The `add` field of the `ShiftMkCore` structure for the induced shift.  -/
CategoryTheory.HasShift.Induced.add : {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) →
          {A : Type u_3} →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                (s : A → CategoryTheory.Functor D D) →
                  ((a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F) →
                    [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] →
                      [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] →
                        (a b : A) → s (a + b) ≅ (s a).comp (s b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.whiskerLeft_η_addCommutator_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G CategoryTheory.AddMonObj.zero)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.AddGrpObj.addCommutator G) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj G (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β}
  (h : l.Balanced), l.Ordered → (Std.DTreeMap.Internal.Impl.insertIfNew k v l h).impl.Ordered
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_eq_empty : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, s.ordConnectedComponent x = ∅ ↔ x ∉ s
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_apply_of_continuous : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] {f : X → R} {g : ContinuousMapZero X R} {x : X},
  Continuous f → f 0 = 0 → (ContinuousMapZero.mkD f g) x = f x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.distinct_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → List.Pairwise (fun a b => (a == b) = false) m.toList
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z}
  {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f)
  (hc : CategoryTheory.Limits.IsColimit c) (f' : CategoryTheory.Limits.Fan Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv (hf.lift f').op =
    hc.desc f'.op
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.isInducing : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → Topology.IsInducing f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.get_revSkipWhile_char_ne : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {h : pos.revSkipWhile c ≠ s.startPos},
  ((pos.revSkipWhile c).prev h).get ⋯ ≠ c
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.lift_unique : ∀ {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} (f g : ProfiniteAddGrp.ProfiniteCompletion.completion G ⟶ P),
  CategoryTheory.CategoryStruct.comp (ProfiniteAddGrp.ProfiniteCompletion.eta G)
        ((CategoryTheory.forget₂ ProfiniteAddGrp.{u} AddGrpCat).map f) =
      CategoryTheory.CategoryStruct.comp (ProfiniteAddGrp.ProfiniteCompletion.eta G)
        ((CategoryTheory.forget₂ ProfiniteAddGrp.{u} AddGrpCat).map g) →
    f = g
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.factors_left_of_inf_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A B : C}
  {X Y : CategoryTheory.Subobject B} {f : A ⟶ B}, (X ⊓ Y).Factors f → X.Factors f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.Data.Opposite
Opposite.instInhabited : {α : Sort u} → [Inhabited α] → Inhabited αᵒᵖ
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- The weak equalizer built from `weakEqualizer.ι f g` is weakly limiting.  -/
CategoryTheory.Limits.weakEqualizerIsWeakEqualizer : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] →
          CategoryTheory.Limits.IsWeakLimit
            (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.weakEqualizer.ι f g) ⋯)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter!_eq_add_one : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      k ∉ t → (f (t.get? k)).isSome = true → (Std.DTreeMap.Internal.Impl.alter! k f t).size = t.size + 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSetLike : {R : Type u} → {M : Type v} → [inst : SMul R M] → SetLike (SubMulAction R M) M
-- Mathlib.GroupTheory.Exponent
AddMonoid.ExponentExists.isOfFinAddOrder : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.ExponentExists G → ∀ {g : G}, IsOfFinAddOrder g
-- Mathlib.Data.Int.Log
/-- `Int.clog b` and `zpow b` (almost) form a Galois connection.  -/
Int.le_zpow_iff_clog_le : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (r ≤ ↑b ^ x ↔ Int.clog b r ≤ x)
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If `x` is a fixed point of `f`, then it is a fixed point of `f^[n]`.  -/
Function.IsFixedPt.iterate : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.IsFixedPt f x → ∀ (n : ℕ), Function.IsFixedPt f^[n] x
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R 2 = 4 * Polynomial.X ^ 2 - 1
-- Batteries.Data.Vector.Lemmas
Vector.getElem?_scanr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {i : ℕ} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as)[i]? = if i < n + 1 then some (Vector.foldr f init (as.drop i)) else none
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂_term_fderiv.eq_1 : ∀ (n : ℤ) (z τ : ℂ),
  jacobiTheta₂_term_fderiv n z τ =
    Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z + ↑Real.pi * Complex.I * ↑n ^ 2 * τ) •
      ((2 * ↑Real.pi * Complex.I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ +
        (↑Real.pi * Complex.I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- The `trajContent` of a cylinder is equal to the integral of its indicator function against
`partialTraj`.  -/
ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {b : ℕ} {S : Set ((i : ↥(Finset.Iic b)) → X ↑i)},
  MeasurableSet S →
    ∀ (x₀ : (n : ℕ) → X n) (a : ℕ),
      (ProbabilityTheory.Kernel.trajContent κ (Preorder.frestrictLe a x₀)) (MeasureTheory.cylinder (Finset.Iic b) S) =
        ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b ((MeasureTheory.cylinder (Finset.Iic b) S).indicator 1) x₀
-- Mathlib.Topology.Algebra.FilterBasis
/-- The neighborhood function of a `GroupFilterBasis`.  -/
GroupFilterBasis.N : {G : Type u} → [inst : Group G] → GroupFilterBasis G → G → Filter G
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.semiringObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) → (j : J) → Semiring ((F.comp (CategoryTheory.forget SemiRingCat)).obj j)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The diagram of finite quotients indexed by finite-index normal subgroups of `G`.  -/
ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram : (G : GrpCat) → CategoryTheory.Functor (FiniteIndexNormalSubgroup ↑G) FiniteGrp.{u}
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.op_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (h : G ⊣ F),
  h.op.counit = CategoryTheory.NatTrans.op h.unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  {f : (a : α) → β a → Bool} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter! f t) = true →
      Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.inv : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : Group β] [MeasurableInv β],
  MeasureTheory.IsProgressive f u → MeasureTheory.IsProgressive f fun i ω => (u i ω)⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_cons : ∀ {V : Type u_1} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj w u),
  p.IsSubwalk (SimpleGraph.Walk.cons h p)
-- Init.Data.SInt.Lemmas
Int64.lt_asymm : ∀ {a b : Int64}, a < b → ¬b < a
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- If `G` is a group acting multiplicatively on a set, then the action is transitive if there is
a single element whose orbit is everything.  -/
MulAction.IsPretransitive.of_orbit : ∀ {G : Type u_2} {X : Type u_5} [inst : Group G] [inst_1 : MulAction G X] {x₀ : X},
  (∀ (x : X), ∃ g, g • x₀ = x) → MulAction.IsPretransitive G X
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.biInter : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β},
  s.Countable → (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋂ b ∈ s, f b)
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant
is 1. (This definition is only correct if 2 is invertible.)  -/
Matrix.specialUnitaryGroup : (n : Type u) →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → (α : Type v) → [inst_2 : CommRing α] → [StarRing α] → Submonoid (Matrix n n α)
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLawfulUpwardEnumerableLTNat : Std.PRange.LawfulUpwardEnumerableLT ℕ
-- Mathlib.RingTheory.Morita.Basic
/-- For any `R`-algebras `A`, `B`, and `C`, if `A` is Morita equivalent to `B` and `B` is Morita
equivalent to `C`, then `A` is Morita equivalent to `C`.
 -/
MoritaEquivalence.trans : (R : Type u₀) →
  [inst : CommSemiring R] →
    {A B C : Type u₁} →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          [inst_3 : Ring B] →
            [inst_4 : Algebra R B] →
              [inst_5 : Ring C] →
                [inst_6 : Algebra R C] → MoritaEquivalence R A B → MoritaEquivalence R B C → MoritaEquivalence R A C
-- Mathlib.Algebra.Lie.Weights.Linear
/-- The kernel of a weight of a Lie module with linear weights.  -/
LieModule.Weight.ker : {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] →
                      [LieModule.LinearWeights R L M] → {χ : LieModule.Weight R L M} → Submodule R L
-- Init.Data.List.Lemmas
List.tail?_append : ∀ {α : Type u_1} {l l' : List α}, (l ++ l').tail? = (Option.map (fun x => x ++ l') l.tail?).or l'.tail?
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_iSup_of_mem : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] {S : ι → Subsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
-- Lean.Meta.Tactic.Try.Collect
_private.Lean.Meta.Tactic.Try.Collect.0.Lean.Meta.Try.collect.unsafe_impl_2 : Lean.MVarId → Lean.Try.Config → Lean.MetaM Lean.Meta.Try.Collector.Result
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.measurable_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  Measurable (s.rnDeriv μ)
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod : Lean.Name → IO (Array (Lean.ModuleData × Lean.CompactedRegion))
-- Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
contDiffOn_succ_iff_fderiv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}
  {f : D → E} {s : Set D} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 D],
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (n + 1) f s ↔
      DifferentiableOn 𝕜 f s ∧
        (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ∀ (y : D), ContDiffOn 𝕜 n (fun x => (fderivWithin 𝕜 f s x) y) s)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.sub_eq_zero' : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r : R}
  (hr : r ∈ S), r -ₒ ⟨r, hr⟩ = 0
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.mem_adjoint_domain_of_exists : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E] (y : F), (∃ w, ∀ (x : ↥T.domain), inner 𝕜 w ↑x = inner 𝕜 y (↑T x)) → y ∈ T.adjoint.domain
-- Std.Time.Time.Unit.Nanosecond
/-- `Ordinal` represents a nanosecond value that is bounded between 0 and 999,999,999 nanoseconds.
 -/
Std.Time.Nanosecond.Ordinal : Type
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_inv : ∀ {K : Type u_1} [inst : RCLike K] (x : K), (starRingEnd K) x⁻¹ = ((starRingEnd K) x)⁻¹
-- Mathlib.Order.CompleteLattice.Basic
/-- A version of `iSup_option` useful for rewriting right-to-left.  -/
iSup_option_elim : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (a : α) (f : β → α), ⨆ o, o.elim a f = a ⊔ ⨆ b, f b
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (n : N₂),
  (RootPairing.Equiv.coweightEquiv P Q e) n = (↑e).coweightMap n
-- Mathlib.Combinatorics.Schnirelmann
/-- To show the Schnirelmann density is upper bounded by `x`, it suffices to show
`|A ∩ {1, ..., n}| / n ≤ x`, for any chosen positive value of `n`.

We provide `n` explicitly here to make this lemma more easily usable in `apply` or `refine`.
This lemma is analogous to `ciInf_le_of_le`.
 -/
schnirelmannDensity_le_of_le : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {x : ℝ} (n : ℕ),
  n ≠ 0 → ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n ≤ x → schnirelmannDensity A ≤ x
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_toBlocks : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n ⊕ o) (l ⊕ m) α),
  Matrix.fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
/-- If an integrable function has zero integral on all compact sets in a sigma-compact space, then
it is zero almost everywhere.  -/
MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3}
  [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [BorelSpace β] [SigmaCompactSpace β] [R1Space β]
  {μ : MeasureTheory.Measure β} {f : β → E},
  MeasureTheory.Integrable f μ → (∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0) → f =ᵐ[μ] 0
-- Mathlib.Logic.Nonempty
nonempty_psigma : ∀ {α : Sort u_4} {β : α → Sort u_3}, Nonempty (PSigma β) ↔ ∃ a, Nonempty (β a)
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toStalk_smul : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (r : R)
  (m : ↑((AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x)),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R x)) r • m = r • m
-- Mathlib.Data.Real.Sign
Real.sign_mul_nonneg : ∀ (r : ℝ), 0 ≤ r.sign * r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKey? k = if (f (t.get? k)).isSome = true then some k else none
-- Init.Data.Vector.Lemmas
Vector.decide_exists_mem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Prop} [inst : DecidablePred p],
  decide (∃ x ∈ xs, p x) = xs.any fun b => decide (p b)
-- Mathlib.Logic.Equiv.Basic
Equiv.trans_swap_trans_symm : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a b : β) (e : α ≃ β),
  (e.trans (Equiv.swap a b)).trans e.symm = Equiv.swap (e.symm a) (e.symm b)
-- Mathlib.Data.Multiset.DershowitzManna
/-- Over a well-founded order, the Dershowitz-Manna order on multisets is well-founded.  -/
Multiset.wellFounded_isDershowitzMannaLT : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedLT α], WellFounded Multiset.IsDershowitzMannaLT
-- Aesop.Tree.TreeM
Aesop.TreeM.run' : {α : Type} → Aesop.TreeM.Context → Aesop.Tree → Aesop.TreeM α → Aesop.BaseM (α × Aesop.TreeM.State)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.carrier_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  ConjRootClass.carrier 0 = {0}
-- Mathlib.Order.LatticeIntervals
Set.Iic.disjoint_iff : ∀ {α : Type u_1} {a : α} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {x y : ↑(Set.Iic a)},
  Disjoint x y ↔ Disjoint ↑x ↑y
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueD k' (Std.Internal.List.Const.alterKey k f l) fallback =
      if (k == k') = true then (f (Std.Internal.List.getValue? k l)).getD fallback
      else Std.Internal.List.getValueD k' l fallback