mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalProperties.Projective
LinearMap.split_surjective_of_localization_maximal : ∀ {R : Type u_1} {N : Type u_2} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) [Module.FinitePresentation R N],
  (∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = LinearMap.id) →
    ∃ g, f ∘ₗ g = LinearMap.id
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is strictly between the other two, the oriented angle at the
third point (reversed) is zero.  -/
Sbtw.oangle₁₃₂_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₁ p₃ p₂ = 0
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.of.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [inst_1 : SizeOf J]
  (j : J) (x : ↑(F.obj j)), sizeOf (CommRingCat.Colimits.Prequotient.of j x) = 1 + sizeOf j + sizeOf x
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.measurable_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [inst_1 : MeasurableSpace β] [BorelSpace β] (f : ↥(MeasureTheory.Lp β 1 μ)), Measurable ↑↑f
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedNatTrans.mk : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {F G : CategoryTheory.EnrichedFunctor V C D} → (F.forget ⟶ G.forget) → CategoryTheory.EnrichedNatTrans F G
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_lt_ofNat : ∀ {n x y : ℕ}, BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2 ^ n < y % 2 ^ n
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.contains.eq_1 : ∀ (s : String) (c : Char), String.Legacy.contains s c = String.Legacy.any s fun a => a == c
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.mulVec_empty : ∀ {α : Type u} {m' : Type uₘ} [inst : NonUnitalNonAssocSemiring α] (A : Matrix m' (Fin 0) α) (v : Fin 0 → α),
  A.mulVec v = 0
-- Mathlib.Analysis.Calculus.Deriv.ZPow
DifferentiableOn.zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {m : ℤ} {f : E → 𝕜} {t : Set E},
  DifferentiableOn 𝕜 f t → (∀ x ∈ t, f x ≠ 0) ∨ 0 ≤ m → DifferentiableOn 𝕜 (fun x => f x ^ m) t
-- Mathlib.Order.Category.Lat
Lat.ext : ∀ {X Y : Lat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.mk.inj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {functor : CategoryTheory.Functor C₁ C₂}
  {map : W₁ ≤ W₂.inverseImage functor} {functor_1 : CategoryTheory.Functor C₁ C₂}
  {map_1 : W₁ ≤ W₂.inverseImage functor_1},
  { functor := functor, map := map } = { functor := functor_1, map := map_1 } → functor = functor_1
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncate_wittVector_truncate : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) (x : WittVector p R),
  (TruncatedWittVector.truncate hm) ((WittVector.truncate m) x) = (WittVector.truncate n) x
-- Mathlib.Algebra.Star.Subalgebra
/-- Restriction of the codomain of a `StarAlgHom` to its range.  -/
StarAlgHom.rangeRestrict : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] →
              [inst_4 : StarRing A] →
                [inst_5 : Semiring B] →
                  [inst_6 : Algebra R B] →
                    [inst_7 : StarRing B] → [inst_8 : StarModule R B] → (f : A →⋆ₐ[R] B) → A →⋆ₐ[R] ↥f.range
-- Lean.Elab.Tactic.Grind.Config
/-- Elaborator for grind configurations, with the `(config := ...)` elaborator exposed.
This allows overriding which structure is used as the expected type when elaborating
the term, which affects which default values are used in `{...}` structure instance notation.
 -/
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.elabGrindConfigCore : (Lean.Term → Lean.Elab.TermElabM Lean.Grind.Config) →
  Lean.Syntax → optParam Lean.Grind.Config { } → optParam Bool true → Lean.Elab.TermElabM Lean.Grind.Config
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_pow : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Pow β M] (c : M) (f : α → β),
  UniformFun.ofFun (f ^ c) = UniformFun.ofFun f ^ c
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split_ineq_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- The entropy of an entourage `U`, defined as the exponential rate of growth of the size of the
largest `(U, n)`-dynamical net of `F`. Takes values in the space of extended real numbers
`[-∞,+∞]`. This version uses a `liminf`, and is an alternative definition.  -/
Dynamics.netEntropyInfEntourage : {X : Type u_1} → (X → X) → Set X → SetRel X X → EReal
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- The set of all `n` such that `X^n` has a non-zero coefficient.
 -/
SkewPolynomial.support : {R : Type u_1} → [inst : Semiring R] → SkewPolynomial R → Finset ℕ
-- Lean.Syntax
/-- Like `eqWithInfo` but prints trace on failure if `trace.Elab.reuse` is activated.  -/
Lean.Syntax.eqWithInfoAndTraceReuse : Lean.Options → Lean.Syntax → Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            (CategoryTheory.NonemptyParallelPairPresentationAux.F₂ f g P₁ P₂).comp CategoryTheory.yoneda ⟶
              (CategoryTheory.Functor.const (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂)).obj B
-- Init.Core
/-- `x != y` is boolean not-equal. It is the negation of `x == y` which is supplied by
the `BEq` typeclass.

Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead of
`Prop` valued. It is mainly intended for programming applications.


Conventions for notations in identifiers:

 * The recommended spelling of `!=` in identifiers is `bne`. -/
«term_!=_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Image
Set.subset_range_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ (s : Set β), s ⊆ Set.range f
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.LiftCommShift.iso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (r : HomRel C) {A : Type w} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : r.IsCompatibleWithShift A]
  [inst_6 : F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A) (X : C),
  (CategoryTheory.Quotient.LiftCommShift.iso F r hF a).hom.app ((CategoryTheory.Quotient.functor r).obj X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Quotient.lift r F hF).map
        ((CategoryTheory.Functor.commShiftIso (CategoryTheory.Quotient.functor r) a).inv.app X))
      ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  a < b →
    MeasureTheory.upcrossingsBefore a b f N ω < n →
      MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.upperCrossingTime a b f N (n + 1) ω)) ω -
          MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.lowerCrossingTime a b f N n ω)) ω =
        0
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a finite Galois group for `L/K`, `H` is a Galois group for `L/E`, and `E/K` is
Galois, then `H` is a normal subgroup of `G`.  -/
IsGaloisGroup.normal_of_isGalois : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] (E : Type u_5)
  [inst_5 : Field E] [inst_6 : Algebra K E] [inst_7 : Algebra E L] [IsScalarTower K E L] [Finite G]
  [IsGaloisGroup (↥H) E L] [IsGalois K E], H.Normal
-- Mathlib.Order.Defs.Unbundled
trans_trichotomous_left : ∀ {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [Std.Trichotomous r] {a b c : α}, ¬r b a → r b c → r a c
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commRing.injEq : ∀ (id id_1 : ℕ),
  (Lean.Meta.Sym.Arith.ClassifyResult.commRing id = Lean.Meta.Sym.Arith.ClassifyResult.commRing id_1) = (id = id_1)
-- Mathlib.Data.Set.Function
Set.MapsTo.inter_inter : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.MapsTo f s₁ t₁ → Set.MapsTo f s₂ t₂ → Set.MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂)
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt16 = OfNat.ofNat n
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_4)
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence],
  (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G A).inverse = G.sheafPushforwardContinuous A J K
-- Mathlib.Topology.Homotopy.Product
ContinuousMap.HomotopyRel.prod_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {A : Type u_3}
  [inst_2 : TopologicalSpace A] {f₀ f₁ : C(A, α)} {g₀ g₁ : C(A, β)} {S : Set A} (F : f₀.HomotopyRel f₁ S)
  (G : g₀.HomotopyRel g₁ S) (t : ↑unitInterval × A), (F.prod G) t = (F t, G t)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.omega0_opow_epsilon : ∀ (o : Ordinal.{u_1}), Ordinal.omega0 ^ o.epsilon = o.epsilon
-- Mathlib.Topology.Category.TopPair
/-- A homotopy of maps between topological pairs is a homotopy on the first space and a homotopy on
the second space that fit in a commutative square with the maps of the pairs.  -/
TopPair.Homotopy : {X Y : TopPair} → (X ⟶ Y) → (X ⟶ Y) → Type u
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₃_of_memoizedLeft : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Productive α₂ m] {it' it : Std.IterM m (β₁ × β₂)},
  Option.SomeLtNone.lt emptyRelation it'.internalState.memoizedLeft it.internalState.memoizedLeft →
    Std.Iterators.Types.Zip.Rel₃ m it' it
-- Init.Data.Fin.Lemmas
Fin.succ_eq_last_succ : ∀ {n : ℕ} {i : Fin n.succ}, i.succ = Fin.last (n + 1) ↔ i = Fin.last n
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_compatibility : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (L₁ : CategoryTheory.Functor C D) (L₂ : CategoryTheory.Functor C E) [inst_3 : L₁.IsLocalization W]
  [inst_4 : L₂.IsLocalization W],
  (CategoryTheory.Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).hom.app X)
      (CategoryTheory.CategoryStruct.comp (φ.map L₂ ⋯)
        ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).inv.app Y))
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `R0Space.specializes_symm`.

---

In an R₀ space, the `Specializes` relation is symmetric.  -/
R0Space.specializes_symmetric : ∀ {X : Type u} {inst : TopologicalSpace X} [self : R0Space X], Std.Symm Specializes
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.CancelParams.mk.inj : ∀ {id id_1 : Lean.JsonRpc.RequestID}, { id := id } = { id := id_1 } → id = id_1
-- Mathlib.CategoryTheory.Equivalence
/-- As a special case, given two equivalences `G` and `G'` between the same categories,
construct an isomorphism `G.functor ≅ G.functor` from an isomorphism `G.inverse ≅ G.inverse`.  -/
CategoryTheory.Iso.isoFunctorOfIsoInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {G G' : C ≌ D} → (G.inverse ≅ G'.inverse) → (G.functor ≅ G'.functor)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
/-- The vertical strip of width `A` and height `B`, defined by elements whose real part has absolute
value less than or equal to `A` and imaginary part is at least `B`.  -/
UpperHalfPlane.verticalStrip : ℝ → ℝ → Set UpperHalfPlane
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.convs'Aux_stable_step_of_terminated : ∀ {K : Type u_1} {n : ℕ} [inst : DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)},
  s.TerminatedAt n → GenContFract.convs'Aux s (n + 1) = GenContFract.convs'Aux s n
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.move.inj : ∀ {Γ : Type u_1} {a a_1 : Turing.Dir}, Turing.TM0.Stmt.move a = Turing.TM0.Stmt.move a_1 → a = a_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
/-- A version of `CliffordAlgebra.ι` that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide `CliffordAlgebra.gradedAlgebra`.  -/
CliffordAlgebra.GradedAlgebra.ι : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → M →ₗ[R] DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.node.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α) (child sibling : Batteries.BinomialHeap.Imp.HeapNode α),
  sizeOf (Batteries.BinomialHeap.Imp.HeapNode.node a child sibling) = 1 + sizeOf a + sizeOf child + sizeOf sibling
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isInaccessible_def : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible ↔ Cardinal.aleph0 < c ∧ c.IsRegular ∧ c.IsStrongLimit
-- Init.Data.Char.Lemmas
Char.ltAsymm : Std.Asymm fun x1 x2 => x1 < x2
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldlM.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (x : δ) (x_1 : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldlM f x x_1 =
    match x, x_1 with
    | d, Std.DHashMap.Internal.AssocList.nil => pure d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => do
      let d ← f d a b
      Std.DHashMap.Internal.AssocList.foldlM f d es
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.bot_toAddSubmonoid : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊥.toAddSubmonoid = ⊥
-- Mathlib.Combinatorics.Nullstellensatz
/-- The support of `Alon.P S i` is the set of exponents of the form `single i e`,
for `e ≤ S.card`.  -/
_private.Mathlib.Combinatorics.Nullstellensatz.0.MvPolynomial.Alon.of_mem_P_support : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_3} (i : ι) (S : Finset R),
  ∀ m ∈ (MvPolynomial.Alon.P✝ S i).support, ∃ e ≤ S.card, m = fun₀ | i => e
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddRightCancelSemigroup : {α : Type u_1} → [AddRightCancelSemigroup α] → AddRightCancelSemigroup αᵐᵒᵖ
-- Mathlib.Data.Finset.Preimage
Finset.image_eq_preimage_of_leftInvOn_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {g : β → α} {s : Finset α},
  Set.LeftInvOn g f ↑s → ∀ (ginj : Set.InjOn g (g ⁻¹' ↑s)), Finset.image f s = s.preimage g ginj
-- Init.Data.List.MinMax
List.min?_cons' : ∀ {α : Type u_1} {x : α} [inst : Min α] {xs : List α}, (x :: xs).min? = some (List.foldl min x xs)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.smul_apply : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] (b : R) (v : DirectSum ι fun i => M i) (i : ι), (b • v) i = b • v i
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.productive_dropn : ∀ {α : Type u} (s : Stream'.WSeq α) [s.Productive] (n : ℕ), (s.drop n).Productive
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.instSMul' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_3} →
            [inst_3 : SMul S R] → [inst_4 : SMul S M] → [IsScalarTower S R M] → (P : Submodule R M) → SMul S (M ⧸ P)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasDerivAt_exp_smul_const_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) * x) t
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  k' ∈ m.alter k f ↔ if (k == k') = true then (f (m.get? k)).isSome = true else k' ∈ m
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : RBTree.RBMap α β cmp) (k : α),
  t.find? k = Option.map (fun x => x.2) (t.findEntry? k)
-- Mathlib.Topology.MetricSpace.Thickening
IsCompact.exists_thickening_image_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : PseudoEMetricSpace β] {f : α → β} {K : Set α}
  {U : Set β},
  IsCompact K →
    IsOpen U →
      (∀ x ∈ K, ContinuousAt f x) → Set.MapsTo f K U → ∃ ε > 0, ∃ V ∈ nhdsSet K, Metric.thickening ε (f '' V) ⊆ U
-- Lean.Server.Rpc.Basic
Lean.Lsp.instHashableRpcRef : Hashable Lean.Lsp.RpcRef
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInverseAssociator_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D ⊕ E),
  (CategoryTheory.sum.inrCompInverseAssociator C D E).inv.app X =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).sum'
            (CategoryTheory.Sum.inr_ (C ⊕ D) E)).obj
        X)
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported.eq_1 : ∀ {σ : Type u_1} (R : Type u) [inst : CommSemiring R] (s : Set σ),
  MvPolynomial.supported R s = Algebra.adjoin R (MvPolynomial.X '' s)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.homEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (self : F.RepresentableBy Y) {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
  self.homEquiv (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (self.homEquiv g)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.le_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {f : M →ₙ* N},
  S ≤ Subsemigroup.comap f (Subsemigroup.map f S)
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.neg_right_iff : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a (-b) ↔ AddCommute a b
-- Init.Data.Vector.Lex
Vector.le_total : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] (xs ys : Vector α n), xs ≤ ys ∨ ys ≤ xs
-- Init.Data.SInt.Bitwise
Int64.toUInt64_and : ∀ (a b : Int64), (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
/-- At `x=0`, `(fun x ↦ x * log x)` is not differentiable
(but note that it is continuous, see `continuous_mul_log`).  -/
Real.not_DifferentiableAt_log_mul_zero : ¬DifferentiableAt ℝ (fun x => x * Real.log x) 0
-- Mathlib.Analysis.Normed.Group.Int
norm_zsmul_le : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] (n : ℤ) (a : α), ‖n • a‖ ≤ ‖n‖ * ‖a‖
-- Mathlib.NumberTheory.ModularForms.Cusps
ModularGroup.T.eq_1 : ModularGroup.T = ⟨!![1, 1; 0, 1], ModularGroup.T._proof_1⟩
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.range_comp_incl_top : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), (f.comp (NormedAddGroupHom.incl ⊤)).range = f.range
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).getKey! k = t₂.getKeyD k (t₁.getKey! k)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_ofList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.ExtTreeSet.ofList l cmp).size ≤ l.length
-- Mathlib.Data.QPF.Multivariate.Basic
/-- Every polynomial functor is a (trivial) QPF  -/
MvPFunctor.instMvQPFObj : {n : ℕ} → (P : MvPFunctor.{u_1} n) → MvQPF ↑P
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadInfo.mk.sizeOf_spec : ∀ (check : Lean.Elab.Term.Quotation.HeadCheck)
  (onMatch : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult)
  (doMatch :
    (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term),
  sizeOf { check := check, onMatch := onMatch, doMatch := doMatch } = 1 + sizeOf check
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The sum of two `C^n` functions at a point is `C^n` at this point.  -/
ContDiffAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {f g : E → F}, ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => f x + g x) x
-- Mathlib.Order.Bounds.Image
mem_upperBounds_image2_of_mem_lowerBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → a ∈ lowerBounds s → b ∈ lowerBounds t → f a b ∈ upperBounds (Set.image2 f s t)
-- Lean.DocString.Types
Lean.Doc.Inline.brecOn_2.go : {i : Type u} →
  {motive_1 : Lean.Doc.Inline i → Sort u_1} →
    {motive_2 : Array (Lean.Doc.Inline i) → Sort u_1} →
      {motive_3 : List (Lean.Doc.Inline i) → Sort u_1} →
        (t : List (Lean.Doc.Inline i)) →
          ((t : Lean.Doc.Inline i) → t.below → motive_1 t) →
            ((t : Array (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_1 t → motive_2 t) →
              ((t : List (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_2 t → motive_3 t) →
                motive_3 t ×' Lean.Doc.Inline.below_2 t