mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Finiteness
/-- If there exists a finite set `{ r }` of `R` that generates the unit ideal and such that `Mᵣ` is
`Rᵣ`-finite for each `r`, then `M` is a finite `R`-module.

See `of_localizationSpan` for a version without the finite set assumption.
 -/
Module.Finite.of_localizationSpan_finite : ∀ {R : Type u} [inst : CommSemiring R] {M : Type w} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (t : Finset R),
  Ideal.span ↑t = ⊤ →
    (∀ (g : ↥t), Module.Finite (Localization.Away ↑g) (LocalizedModule.Away (↑g) M)) → Module.Finite R M
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The term in `MapFactorizationData (W₁.inverseImage F) (W₂.inverseImage F) f`
deduced from `h : MapFactorizationData W₁ W₂ (F.map f)` when `F` is an equivalence
of categories and both `W₁` and `W₂` respect isomorphisms.  -/
CategoryTheory.MorphismProperty.MapFactorizationData.ofIsEquivalence : {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₁ W₂ : CategoryTheory.MorphismProperty C} →
          {F : CategoryTheory.Functor D C} →
            [F.IsEquivalence] →
              [W₁.RespectsIso] →
                [W₂.RespectsIso] →
                  {X Y : D} →
                    {f : X ⟶ Y} →
                      W₁.MapFactorizationData W₂ (F.map f) →
                        (W₁.inverseImage F).MapFactorizationData (W₂.inverseImage F) f
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Coercion of a `MulHom` into a function is itself a `MulHom`.

See also `MulHom.eval`.  -/
MulHom.coeFn : (α : Type u_5) → (β : Type u_6) → [inst : Mul α] → [inst_1 : CommSemigroup β] → (α →ₙ* β) →ₙ* α → β
-- Init.Data.Float.Model.Unpacked.Operations.Compare
/-- Determines whether `a` is less than `b` according to IEEE rules.

This is not a total ordering.
 -/
Float.Model.UnpackedFloat.lt : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.roots_U_real_nodup : ∀ (n : ℕ), (Multiset.map (fun k => Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (Multiset.range n)).Nodup
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst : ∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X)
  (x :
    ↑(CommRingCat.of
        ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus
            ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
              (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V))))))),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op))
      ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) =
    (↑x).1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.subOneIntegralPowerBasis_gen : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n), hζ.subOneIntegralPowerBasis.gen = ⟨ζ - 1, ⋯⟩
-- Lean.DocString.Parser
/-- Parses bold: a matched pair of one or more `*`.
 -/
Lean.Doc.Parser.bold : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for nonnegative `p : ℝ` and any `x ∈ [0, |t|)`,
`|X| ^ p * exp (v * X + x * |X|)` is integrable.  -/
ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v x : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
      0 ≤ x →
        x < |t| → ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun a => |X a| ^ p * Real.exp (v * X a + x * |X a|)) μ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_le_size_insertMany : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : ρ}, (↑m).size ≤ (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).size
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- Shows that for any `q : ℚ` with `0 < q < 1`, the numerator of the fractional part of
`IntFractPair.of q⁻¹` is smaller than the numerator of `q`.
 -/
GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos : ∀ {q : ℚ}, 0 < q → (GenContFract.IntFractPair.of q⁻¹).fr.num < q.num
-- Batteries.Tactic.PrintOpaques
/-- The monad used by `CollectOpaques`.  -/
Batteries.Tactic.CollectOpaques.M : Type → Type
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.loop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.not_gt` -/
LE.le.not_ssuperset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊂ a
-- Mathlib.Analysis.Calculus.FDeriv.Pow
differentiable_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ), Differentiable 𝕜 fun x => x ^ n
-- Mathlib.Topology.MetricSpace.Bounded
CauchySeq.isBounded_range : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α}, CauchySeq f → Bornology.IsBounded (Set.range f)
-- Std.Sat.AIG.CNF
/-- The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State : Std.Sat.AIG ℕ → Type
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxo.HasSize α] [inst_1 : Std.PRange.UpwardEnumerable α] (r : Std.Roo α),
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some lower => Std.Rxo.HasSize.size lower r.upper
-- Std.Data.HashMap.Lemmas
Std.HashMap.foldM_eq_foldlM_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.HashMap.foldM (fun d a x => f d a) init m = List.foldlM f init m.keys
-- Init.Data.BitVec.Lemmas
BitVec.intMin.eq_1 : ∀ (w : ℕ), BitVec.intMin w = BitVec.twoPow w (w - 1)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_zero_left : ∀ (x : Ordinal.{u_1}), Ordinal.log 0 x = 0
-- Mathlib.Topology.Order.Monotone
/-- **Alias** of `MonotoneOn.countable_setOfPred_two_preimages`.

---

If a function is monotone on a set in a second countable topological space, then there
are only countably many points that have several preimages.  -/
MonotoneOn.countable_setOf_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α],
  MonotoneOn f s → {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_π : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))]
  (h : CategoryTheory.Limits.IsTerminal Y₃),
  (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).π = (G.map f₁.op).app X₃
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The characterization of weak convergence of probability measures by the condition that the
integrals of every continuous bounded nonnegative function are continuous.  -/
MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.ProbabilityMeasure Ω},
  Continuous μs ↔ ∀ (f : BoundedContinuousFunction Ω NNReal), Continuous fun x => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_antitone : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F), Antitone ⇑T.singularValues
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.lt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (f : Std.PRange.UpwardEnumerable.Map α β) {a b : α},
  Std.PRange.UpwardEnumerable.LT a b ↔ Std.PRange.UpwardEnumerable.LT (f.toFun a) (f.toFun b)
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Max α] [inst_1 : Bot α], SupBotHom.instInhabited α = { default := SupBotHom.id α }
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.comp_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Comonad C} (f : T₁ ⟶ T₂)
  (g : T₂ ⟶ T₃),
  (CategoryTheory.CategoryStruct.comp f g).toNatTrans = CategoryTheory.CategoryStruct.comp f.toNatTrans g.toNatTrans
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel α β` from a `Kernel α (β × γ)` by taking the map of the first projection.
We use `mapOfMeasurable` for better defeqs.  -/
ProbabilityTheory.Kernel.fst : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel α (β × γ) → ProbabilityTheory.Kernel α β
-- Mathlib.NumberTheory.SmoothNumbers
Nat.smoothNumbers_zero : Nat.smoothNumbers 0 = {1}
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.Const.alterₘ.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isColocal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (X : C),
  W.isColocal X ↔ ∀ ⦃Y Z : C⦄ (g : Y ⟶ Z), W g → Function.Bijective fun f => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Analysis.Complex.Angle
/-- Chord-length is always greater than a multiple of arc-length.  -/
Complex.mul_angle_le_norm_sub : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → 2 / Real.pi * InnerProductGeometry.angle x y ≤ ‖x - y‖
-- Mathlib.Order.CompleteBooleanAlgebra
iInf_iSup_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompletelyDistribLattice α] {f : (a : ι) → κ a → α},
  ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_val_iff : ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂
-- Mathlib.CategoryTheory.ObjectProperty.Shift
/-- Given a predicate `P : C → Prop` on objects of a category equipped with a shift by `A`,
this is the predicate which is satisfied by `X` if `P (X⟦a⟧)`.  -/
CategoryTheory.ObjectProperty.shift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      {A : Type u_2} → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → A → CategoryTheory.ObjectProperty C
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkMixfix : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_subset_add_left : ∀ {α : Type u_2} [inst : Add α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → (↑m₁).size = (↑m₂).size
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_image_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {s : Set β},
  Bornology.IsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.instCanonicallyOverSpecStalkCommRingCatPresheaf : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → (AlgebraicGeometry.Spec (X.presheaf.stalk x)).CanonicallyOver X
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.comap_top : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L), Subfield.comap f ⊤ = ⊤
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {l : List (Equiv.Perm α)},
  (∀ g ∈ l, g.IsSwap) → (l.prod ∈ alternatingGroup α ↔ Even l.length)
-- Mathlib.Tactic.Order
/-- Implementation of `orderCore` in `AtomM`.  -/
Mathlib.Tactic.Order.orderCoreImp : Bool → Array Lean.Expr → Lean.Expr → Lean.MVarId → Mathlib.Tactic.AtomM Unit
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (m.alter k f).getKey? k' = if (k == k') = true then if (f m[k]?).isSome = true then some k else none else m.getKey? k'
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The refl quiver underlying a nerve is isomorphic to the refl quiver underlying the category.  -/
SSet.OneTruncation₂.ofNerve₂ : (C : Type u) →
  [inst : CategoryTheory.Category.{u, u} C] →
    CategoryTheory.ReflQuiv.of (SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve C))) ≅
      CategoryTheory.ReflQuiv.of C
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_univ : ∀ {α : Type u_1} {r : α → α → Prop}, Set.univ.Pairwise r ↔ Pairwise r
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tendsto_coe' : ∀ {α : Type u_2} {f : Filter α} [f.NeBot] {m : α → NNReal} {x : ℝ},
  Filter.Tendsto (fun a => ↑(m a)) f (nhds x) ↔ ∃ (hx : 0 ≤ x), Filter.Tendsto m f (nhds ⟨x, hx⟩)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {x : A}, x ∈ ⊤
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instDecidableEqOfLawfulEqCmpOfTransCmpOfLawfulBEq : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → [Std.TransCmp cmp] → [inst : BEq β] → [LawfulBEq β] → DecidableEq (Std.ExtTreeMap α β cmp)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
neg_iff_pos_of_mul_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
  [AddRightMono R] [AddRightReflectLE R], a * b < 0 → (a < 0 ↔ 0 < b)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.instInhabited_fg : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → Inhabited { S // S.FG }
-- Mathlib.Order.Lattice.Congruence
LatticeCon.mk : {α : Type u_2} →
  [inst : Lattice α] →
    (toSetoid : Setoid α) →
      (∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊓ y) (x ⊓ z)) →
        (∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊔ y) (x ⊔ z)) → LatticeCon α
-- Std.Do.PredTrans
Std.Do.PredTrans.instLE : {ps : Std.Do.PostShape} → {α : Type u} → LE (Std.Do.PredTrans ps α)
-- Init.Data.Nat.Gcd
Nat.gcd_sub_self_right : ∀ {m n : ℕ}, m ≤ n → m.gcd (n - m) = m.gcd n
-- Mathlib.LinearAlgebra.BilinearMap
/-- Create a bilinear map from a function that is linear in each component.
See `mk₂` for the special case where both arguments come from modules over the same ring.  -/
LinearMap.mk₂' : (R : Type u_1) →
  (S : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {M : Type u_5} →
          {N : Type u_7} →
            {Pₗ : Type u_11} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : AddCommMonoid Pₗ] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module S N] →
                        [inst_7 : Module R Pₗ] →
                          [inst_8 : Module S Pₗ] →
                            [inst_9 : SMulCommClass S R Pₗ] →
                              (f : M → N → Pₗ) →
                                (∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) →
                                  (∀ (c : R) (m : M) (n : N), f (c • m) n = c • f m n) →
                                    (∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) →
                                      (∀ (c : S) (m : M) (n : N), f m (c • n) = c • f m n) → M →ₗ[R] N →ₗ[S] Pₗ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_eq_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.range_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], NonUnitalAlgHom.range (NonUnitalAlgHom.id R A) = ⊤
-- Mathlib.Topology.Constructions
Filter.Tendsto.finCons : ∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : Y → A 0}
  {g : Y → (j : Fin n) → A j.succ} {l : Filter Y} {x : A 0} {y : (j : Fin n) → A j.succ},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun a => Fin.cons (f a) (g a)) l (nhds (Fin.cons x y))
-- Mathlib.Order.WithBot
WithTop.untop.congr_simp : ∀ {α : Type u_1} (x x_1 : WithTop α) (e_x : x = x_1) (a : x ≠ ⊤), x.untop a = x_1.untop ⋯
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderSubobjects] (F : CategoryTheory.Functor D C)
  [F.PreservesMonomorphisms], (P.inverseImage F).IsClosedUnderSubobjects
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- a choice of right adjoint for `L`  -/
CategoryTheory.ComonadicLeftAdjoint.R : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        (L : CategoryTheory.Functor C D) → [self : CategoryTheory.ComonadicLeftAdjoint L] → CategoryTheory.Functor D C
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootForm_symmetric : ∀ {ι : 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) [inst_5 : Fintype ι],
  LinearMap.IsSymm P.RootForm
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.mul.inj : ∀ {x e b : Q(ℕ)} {a : Mathlib.Tactic.Ring.Common.ExBaseNat x} {a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e}
  {a_2 : Mathlib.Tactic.Ring.Common.ExProdNat b} {a_3 : Mathlib.Tactic.Ring.Common.ExBaseNat x}
  {a_4 : Mathlib.Tactic.Ring.Common.ExProdNat e} {a_5 : Mathlib.Tactic.Ring.Common.ExProdNat b},
  Mathlib.Tactic.Ring.Common.ExProdNat.mul a a_1 a_2 = Mathlib.Tactic.Ring.Common.ExProdNat.mul a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- The localization functor `C ⥤ W.Localization'`
that is fixed by the `[HasLocalization W]` instance.  -/
CategoryTheory.MorphismProperty.Q' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) → [inst_1 : W.HasLocalization] → CategoryTheory.Functor C W.Localization'
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.iCycles = h.i
-- Mathlib.Data.Fin.SuccPred
/-- While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply
a generic theorem about `cast`.  -/
Fin.cast_eq_cast : ∀ {n m : ℕ} (h : n = m), Fin.cast h = cast ⋯
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.toOver_obj_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T)
  (X_1 : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)),
  ((CategoryTheory.CostructuredArrow.toOver F X).obj X_1).left = F.obj X_1.left
-- Mathlib.Data.WSeq.Productive
Computation.get.congr_simp : ∀ {α : Type u} (s s_1 : Computation α) (e_s : s = s_1) [h : s.Terminates], s.get = s_1.get
-- Mathlib.Analysis.Fourier.PoissonSummation
/-- **Poisson's summation formula**, assuming that `f` decays as
`|x| ^ (-b)` for some `1 < b` and its Fourier transform is summable.  -/
Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable : ∀ {f : ℝ → ℂ},
  Continuous f →
    ∀ {b : ℝ},
      1 < b →
        (f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) →
          (Summable fun n => FourierTransform.fourier f ↑n) →
            ∀ (x : ℝ), ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x
-- Init.Data.SInt.Lemmas
Int8.toUInt8_neg : ∀ (a : Int8), (-a).toUInt8 = -a.toUInt8
-- Mathlib.Topology.UniformSpace.Defs
uniformContinuous_of_const : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {c : α → β},
  (∀ (a b : α), c a = c b) → UniformContinuous c
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentIdentifier.uri : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.DocumentUri
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_iff_comp_initial_full_faithful : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.Initial] [G.Full] [G.Faithful], F.Initial ↔ (F.comp G).Initial
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.Braided] [inst_7 : F'.Braided] (f : F ⟶ F')
  (X : CategoryTheory.CommGrp C), ((CategoryTheory.Functor.mapCommGrpNatTrans f).app X).hom.hom.hom = f.app X.X
-- Mathlib.Analysis.Asymptotics.Defs
/-- If `u = o(v)` along `l`, then `(u / v) * v = u` eventually at `l`.  -/
Asymptotics.IsLittleO.eventually_mul_div_cancel : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
  u =o[l] v → u / v * v =ᶠ[l] u