mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.prod_mono : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] {S T : NonUnitalSubalgebra R A}
  {S₁ T₁ : NonUnitalSubalgebra R B}, S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.Limits.hasPullback_ofHasPullbacksAgainst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.MorphismProperty C} {c c' c'' : C}
  {f : c ⟶ c'} {g : c'' ⟶ c'} [P.HasPullbacksAgainst P'], P f → P' g → CategoryTheory.Limits.HasPullback f g
-- Mathlib.Logic.Relation
Relation.reflGen_eq_self : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], Relation.ReflGen r = r
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_cons : ∀ {α : Type u_1} (x : α) (xs : FreeAddMonoid α), FreeAddMonoid.toList (x :: xs) = x :: FreeAddMonoid.toList xs
-- Init.Data.Range.Polymorphic.UInt
UInt64.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt64
-- Mathlib.ModelTheory.Syntax
/-- Maps a bounded formula's symbols along a language equivalence.  -/
FirstOrder.Language.LEquiv.onBoundedFormula : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → (L ≃ᴸ L') → L.BoundedFormula α n ≃ L'.BoundedFormula α n
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.eq_zero_of_le_mul_pow : ∀ {x r : ENNReal} {ε : NNReal}, r < 1 → (∀ (n : ℕ), x ≤ ↑ε * r ^ n) → x = 0
-- Lean.Parser.Types
Lean.Parser.ParserState.mkTrailingNode : Lean.Parser.ParserState → Lean.SyntaxNodeKind → ℕ → Lean.Parser.ParserState
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a k : α}
  {v : β k}, (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.brecOn.eq : ∀ {motive_1 : Lean.Lsp.Ipc.ModuleHierarchy → Sort u} {motive_2 : Array Lean.Lsp.Ipc.ModuleHierarchy → Sort u}
  {motive_3 : List Lean.Lsp.Ipc.ModuleHierarchy → Sort u} (t : Lean.Lsp.Ipc.ModuleHierarchy)
  (F_1 : (t : Lean.Lsp.Ipc.ModuleHierarchy) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Lsp.Ipc.ModuleHierarchy.brecOn.go t F_1 F_2 F_3).2
-- Init.Data.Option.Attach
Option.instSubsingletonSubtypeEqSome : ∀ {α : Type u_1} {o : Option α}, Subsingleton { x // o = some x }
-- Init.Prelude
/-- `inferInstance` synthesizes a value of any target type by typeclass
inference. This function has the same type signature as the identity
function, but the square brackets on the `[i : α]` argument means that it will
attempt to construct this argument by typeclass inference. (This will fail if
`α` is not a `class`.) Example:
```
#check (inferInstance : Inhabited Nat) -- Inhabited Nat

def foo : Inhabited (Nat × Nat) :=
  inferInstance

example : foo.default = (default, default) :=
  rfl
```
 -/
inferInstance : {α : Sort u} → [i : α] → α
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_repr_symm : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), ↑b.repr.symm = Finsupp.linearCombination R ⇑b
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X_pow_eq_smul : ∀ {R : Type u} [inst : CommSemiring R] (n k : ℕ),
  (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑(n.descFactorial k) • Polynomial.X ^ (n - k)
-- Std.Data.String.ToInt
String.isInt_comp_toSlice : String.Slice.isInt ∘ String.toSlice = String.isInt
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.mk.sizeOf_spec : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] [inst_3 : SizeOf X] [inst_4 : SizeOf R]
  (toFun : X → X → R) (refl' : ∀ (x : X), toFun x x = 0) (symm' : ∀ (x y : X), toFun x y = toFun y x)
  (triangle' : ∀ (x y z : X), toFun x z ≤ toFun x y + toFun y z),
  sizeOf { toFun := toFun, refl' := refl', symm' := symm', triangle' := triangle' } = 1
-- Mathlib.GroupTheory.Index
MulAction.index_stabilizer_of_transitive : ∀ (G : Type u_1) {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (x : X) [MulAction.IsPretransitive G X],
  (MulAction.stabilizer G x).index = Nat.card X
-- Mathlib.Data.Set.Image
Set.preimage_id_eq : ∀ {α : Type u_1}, Set.preimage id = id
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.mk.sizeOf_spec : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} [inst_2 : SizeOf C] (pt : C) (fst : pt ⟶ P) (snd : pt ⟶ Q) (inl : P ⟶ pt) (inr : Q ⟶ pt)
  (inl_fst :
    autoParam (CategoryTheory.CategoryStruct.comp inl fst = CategoryTheory.CategoryStruct.id P)
      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam)
  (inl_snd :
    autoParam (CategoryTheory.CategoryStruct.comp inl snd = 0) CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam)
  (inr_fst :
    autoParam (CategoryTheory.CategoryStruct.comp inr fst = 0) CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam)
  (inr_snd :
    autoParam (CategoryTheory.CategoryStruct.comp inr snd = CategoryTheory.CategoryStruct.id Q)
      CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam),
  sizeOf
      { pt := pt, fst := fst, snd := snd, inl := inl, inr := inr, inl_fst := inl_fst, inl_snd := inl_snd,
        inr_fst := inr_fst, inr_snd := inr_snd } =
    1 + sizeOf pt + sizeOf fst + sizeOf snd + sizeOf inl + sizeOf inr + sizeOf inl_fst + sizeOf inl_snd +
        sizeOf inr_fst +
      sizeOf inr_snd
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.lift.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : { a // a ≠ 0 } → α)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ = FiniteArchimedeanClass.mk ↑b ⋯ → f a = f b)
  (A : ArchimedeanClass M) (hA : A ≠ ⊤),
  FiniteArchimedeanClass.lift f h ⟨A, hA⟩ =
    (ArchimedeanClass.lift (fun b => if h : b = 0 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A).untop ⋯
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instSeminormedCommRing : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [CompactSpace α] → {R : Type u_4} → [inst_2 : SeminormedCommRing R] → SeminormedCommRing C(α, R)
-- Std.Data.DTreeMap.Basic
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.DTreeMap.diff : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A finite sequence of Lp functions is uniformly integrable.  -/
MeasureTheory.unifIntegrable_finite : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} [Finite ι],
  1 ≤ p → p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_top : ∀ {α : Type u_1} [Nontrivial α], ⊤.diam = 1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.ofIsIso_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.QuasicoherentData), (SheafOfModules.QuasicoherentData.ofIsIso f σ).I = σ.I
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalAddMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y] (x : X),
  LocallyConstant.evalAddMonoidHom x = (Pi.evalAddMonoidHom (fun a => Y) x).comp LocallyConstant.coeFnAddMonoidHom
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The ring of integers adjoined with a square root of `d`.
These have the form `a + b √d` where `a b : ℤ`. The components
are called `re` and `im` by analogy to the negative `d` case.  -/
Zsqrtd : ℤ → Type
-- Init.Data.String.Lemmas.Basic
String.pos.congr_simp : ∀ (s : String) (off off_1 : String.Pos.Raw) (e_off : off = off_1) (h : String.Pos.Raw.IsValid s off),
  s.pos off h = s.pos off_1 ⋯
-- Mathlib.Algebra.Group.TypeTags.Basic
instOneMultiplicativeOfZero : {α : Type u} → [Zero α] → One (Multiplicative α)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_leftUnitor_hom : ∀ {A : Type u_1} {B : Type u_2} (C : Type u_3) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor A B),
  CategoryTheory.Join.mapWhiskerRight F.leftUnitor.hom (CategoryTheory.Functor.id C) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft C (CategoryTheory.Functor.id A) F).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight CategoryTheory.Join.mapPairId.hom
          (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)))
        (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)).leftUnitor.hom)
-- Mathlib.Data.FunLike.IsApply
IsNatCastApply.natCast_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : NatCast F} {inst_2 : SMul ℕ α}
  [self : IsNatCastApply F α] (n : ℕ) (x : α), ↑n x = n • x
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- The actual `NonUnitalSubring` obtained from an element of a `NonUnitalSubringClass`.  -/
NonUnitalSubring.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : SetLike S R] → [NonUnitalSubringClass S R] → S → NonUnitalSubring R
-- Mathlib.Topology.Instances.RatLemmas
Rat.not_firstCountableTopology_opc : ¬FirstCountableTopology (OnePoint ℚ)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished : ∀ {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] (X₁ X₂ : C),
  CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.uliftFunctor_full : CategoryTheory.uliftFunctor.{v, u}.Full
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {F : Type u_1} [inst_5 : FunLike F A B] [inst_6 : AlgHomClass F R A B]
  (f : F), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.Discrete.sumEquiv.match_1.splitter : {J : Type u_1} →
  {K : Type u_2} →
    (motive : J ⊕ K → Sort u_3) →
      (t : J ⊕ K) → ((j : J) → motive (Sum.inl j)) → ((k : K) → motive (Sum.inr k)) → motive t
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- A constant map as a morphism in `CompHausLike`  -/
CompHausLike.const : {P : TopCat → Prop} → (T : CompHausLike P) → {S : CompHausLike P} → ↑S.toTop → (T ⟶ S)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.symm_apply_apply : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (x : M₁),
  f.symm (f x) = x
-- Mathlib.Algebra.Lie.Submodule
/-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
preserved under addition, scalar multiplication and the Lie bracket, then `p` holds for all
elements of the Lie submodule spanned by `s`.  -/
LieSubmodule.lieSpan_induction : ∀ (R : Type u) (L : Type v) {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M} {p : (x : M) → x ∈ LieSubmodule.lieSpan R L s → Prop},
  (∀ (x : M) (h : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : M) (hx : x ∈ LieSubmodule.lieSpan R L s) (hy : y ∈ LieSubmodule.lieSpan R L s),
          p x hx → p y hy → p (x + y) ⋯) →
        (∀ (a : R) (x : M) (hx : x ∈ LieSubmodule.lieSpan R L s), p x hx → p (a • x) ⋯) →
          ∀ {x : M},
            (∀ (x : L) (y : M) (hy : y ∈ LieSubmodule.lieSpan R L s), p y hy → p ⁅x, y⁆ ⋯) →
              ∀ (hx : x ∈ LieSubmodule.lieSpan R L s), p x hx
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State : Type
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.linearIndepOn_coroot : ∀ {ι : 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] {P : RootPairing ι R M N} (self : P.Base),
  LinearIndepOn R ⇑P.coroot ↑self.support
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_map_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] {X Y : C} (φ : X ⟶ Y),
  (t.spectralObjectFunctor.map φ).hom = t.ω₁.whiskerLeft ((CategoryTheory.evaluation C C).map φ)
-- Init.Data.Bool
Bool.le_of_eq : ∀ {x y : Bool}, x = y → x ≤ y
-- Mathlib.Order.Lattice
Function.update_sup : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i)
  (i : ι) (a b : π i), Function.update f i (a ⊔ b) = Function.update f i a ⊔ Function.update f i b
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instMonoid : {α : Type u_1} → [Monoid α] → Monoid (Lex α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.inv_rpow : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), x⁻¹ ^ y = (x ^ y)⁻¹
-- Lean.Util.MonadCache
Lean.instMonadCacheReaderT : {α β ρ : Type} → {m : Type → Type} → [Lean.MonadCache α β m] → Lean.MonadCache α β (ReaderT ρ m)
-- Mathlib.Data.Vector.Basic
List.Vector.tail_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : List.Vector α (n + 1))
  (hp : ∀ x ∈ v.toList, p x), (List.Vector.pmap f v hp).tail = List.Vector.pmap f v.tail ⋯
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The `q`-expansion coefficient can be expressed as a `circleIntegral` for any radius `0 < R < 1`.
 -/
UpperHalfPlane.qExpansion_coeff_eq_circleIntegral : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ (n : ℕ) {R : ℝ},
            0 < R →
              R < 1 →
                (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h f) =
                  (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), UpperHalfPlane.cuspFunction h f z / z ^ (n + 1)
-- Mathlib.Tactic.NormNum.Basic
_private.Mathlib.Tactic.NormNum.Basic.0.Mathlib.Meta.NormNum.Result.add.ratArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : Q(Add «$α»)) → Q(DivisionRing «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» + «$b»))
-- Mathlib.Data.Set.Insert
Set.Nonempty.subset_singleton_iff : ∀ {α : Type u_1} {s : Set α} {a : α}, s.Nonempty → (s ⊆ {a} ↔ s = {a})
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- **Alias** of `SimpleGraph.Walk.support_take`. -/
SimpleGraph.Walk.take_support_eq_support_take_succ : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).support = List.take (n + 1) p.support
-- Mathlib.Data.Set.Semiring
SetSemiring.one_def : ∀ {α : Type u_1} [inst : One α], 1 = Set.up 1
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.eventually_forall_le_atBot : ∀ {α : Type u_3} [inst : Preorder α] {p : α → Prop},
  (∀ᶠ (x : α) in Filter.atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in Filter.atBot, p x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.smul_isBigO : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedRing R] [inst_3 : NormedDivisionRing 𝕜'] {f' : α → E'}
  {g' : α → F'} {l : Filter α} [inst_4 : Module R E'] [IsBoundedSMul R E'] [inst_6 : Module 𝕜' F'] [NormSMulClass 𝕜' F']
  {k₁ : α → R} {k₂ : α → 𝕜'}, k₁ =o[l] k₂ → f' =O[l] g' → (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
-- Mathlib.Data.Fintype.Defs
Fintype.subsingleton : ∀ (α : Type u_4), Subsingleton (Fintype α)
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is
bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r`
form a `Real.HolderTriple`. A version for `NNReal`-valued functions. For an alternative version,
convenient if the infinite sums are already expressed as powers, see `inner_le_Lp_mul_Lq_hasSum`.  -/
NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum : ∀ {ι : Type u} {f g : ι → NNReal} {p q r : ℝ},
  p.HolderTriple q r →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ q) →
        (Summable fun i => (f i * g i) ^ r) ∧
          ∑' (i : ι), (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A morphism of spectral sequences is a sequence of morphisms between the
pages which commutes with the isomorphisms in homology.  -/
CategoryTheory.SpectralSequence.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            CategoryTheory.SpectralSequence C c r₀ → CategoryTheory.SpectralSequence C c r₀ → Type (max u_2 u_3)
-- Std.Async.Select
Std.Async.Selectable.β : {α : Type} → Std.Async.Selectable α → Type
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ),
  groupCohomology.cocyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap (MonoidHom.id G) φ n)
      (groupCohomology.cocyclesMap (MonoidHom.id G) ψ n)
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- Universal property of the radical of a quadratic form:
`Q.radical` is the largest subspace `N` such that
`Q` factors through a quadratic form on `M ⧸ N`.  -/
QuadraticMap.le_radical_iff : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} {N : Submodule R M},
  N ≤ Q.radical ↔ ∃ Q', Q'.comp N.mkQ = Q
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : Lex α), ofLex (a - b) = ofLex a - ofLex b
-- Mathlib.Topology.Order.LowerUpperTopology
/-- A function `f : β → α` with lower topology in the codomain is continuous
if and only if the preimage of every interval `Set.Ici a` is a closed set.
 -/
Topology.IsLower.continuous_iff_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α]
  [inst_3 : TopologicalSpace β] {f : β → α}, Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Ici a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, t.contains a = false → Std.DTreeMap.Const.get! t a = default
-- Mathlib.Data.UInt
USize.toBitVec_nsmul : ∀ (n : ℕ) (a : USize), (n • a).toBitVec = n • a.toBitVec
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList.match_1.congr_eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord M x x_1)
  (h_1 : (i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a))
  (h_2 :
    (x x_3 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord M x j) →
        (_hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_3) → motive x x_3 (w₁.append _hne w₂))
  (i : ι) (x_3 : M i) (a : x_3 ≠ 1),
  x = i →
    x_1 = i →
      x_2 ≍ Monoid.CoprodI.NeWord.singleton x_3 a →
        (match x, x_1, x_2 with
          | i, .(i), Monoid.CoprodI.NeWord.singleton x a => h_1 i x a
          | x, x_4, w₁.append _hne w₂ => h_2 x x_4 j k w₁ _hne w₂) ≍
          h_1 i x_3 a
-- Mathlib.Data.Fintype.Prod
/-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite.  -/
Pi.infinite_of_exists_right : ∀ {ι : Sort u_4} {π : ι → Sort u_5} (i : ι) [Infinite (π i)] [∀ (i : ι), Nonempty (π i)], Infinite ((i : ι) → π i)
-- Init.Data.Nat.Lemmas
Nat.min_self_assoc' : ∀ {m n : ℕ}, min n (min m n) = min n m
-- Mathlib.Data.Vector.MapLemmas
List.Vector.pmap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) {p : β → Prop} (f₁ : (b : β) → p b → γ)
  (f₂ : α → β) (H : ∀ x ∈ (List.Vector.map f₂ xs).toList, p x),
  List.Vector.pmap f₁ (List.Vector.map f₂ xs) H = List.Vector.pmap (fun x hx => f₁ (f₂ x) hx) xs ⋯
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- **Alias** of `AddSubmonoid.NSMulSaturated`.

---

An additive submonoid `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with
`n•g ∈ H` we have `n = 0` or `g ∈ H`. We use the name `NSMulSaturated` to distinguish from
`Submonoid.MulSaturated`.  -/
AddSubgroup.Saturated : {G : Type u_1} → [inst : AddMonoid G] → AddSubmonoid G → Prop
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- `IsDedekindDomain` and `IsDedekindDomainInv` are equivalent ways
to express that an integral domain is a Dedekind domain.  -/
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.isDedekindDomain_iff_isDedekindDomainInv : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A], IsDedekindDomain A ↔ IsDedekindDomainInv✝ A
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.length_map : ∀ {α β β' : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'}, (Std.Iter.map f it).length = it.length
-- Mathlib.Algebra.Order.Sub.Basic
/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order.  -/
tsub_lt_tsub_iff_left_of_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → (a - b < a - c ↔ c < b)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.UnorderedListType.all_complete : ∀ (x : Lean.Doc.Parser.UnorderedListType), x ∈ Lean.Doc.Parser.UnorderedListType.all✝
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.pred_toMul : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : PredOrder X] (x : Additive X),
  Order.pred (Additive.toMul x) = Additive.toMul (Order.pred x)