mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- Equality of linear maps out of an adic completion can be checked on Cauchy sequences.  -/
AdicCompletion.map_ext'' : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f g : AdicCompletion I M →ₗ[R] N},
  f ∘ₗ AdicCompletion.mk I M = g ∘ₗ AdicCompletion.mk I M → f = g
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instAddCommGroup : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → AddCommGroup (TestFunction Ω F n)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_sub_le : ∀ {S : Type u_5} [inst : Ring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Ring R] (abv : R → S)
  [IsAbsoluteValue abv] (a b c : R), abv (a - c) ≤ abv (a - b) + abv (b - c)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (G : Type u)
  [inst_9 : TopologicalSpace G] [inst_10 : ChartedSpace H G] [inst_11 : Group G] [inst_12 : LieGroup I (↑⊤) G]
  (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
  instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M G U =
    { mul := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_1 IM I M G U, mul_assoc := ⋯,
      one := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_4 IM I M G U, one_mul := ⋯, mul_one := ⋯,
      npow := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_8 IM I M G U, npow_zero := ⋯, npow_succ := ⋯,
      inv := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_12 IM I M G U,
      div := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_14 IM I M G U,
      zpow := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_16 IM I M G U, div_eq_mul_inv := ⋯,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Commutativity of the `L^p` product as an isometric equivalence.  -/
IsometryEquiv.withLpProdComm : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] →
        [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → WithLp p (α × β) ≃ᵢ WithLp p (β × α)
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prod_lt_top : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {K : Type u_5} [inst_4 : Field K] [CharZero K] [inst_6 : LieAlgebra K L₁]
  [FiniteDimensional K L₁] {H₁ : LieSubalgebra K L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_8 : LieAlgebra K L₂]
  [FiniteDimensional K L₂] {H₂ : LieSubalgebra K L₂} (b₂ : LieAlgebra.Basis ι₂ H₂),
  (Matrix.reindex eι eι) b₁.A = b₂.A → ∀ [Nontrivial L₂], LieAlgebra.Basis.prod✝ eι b₁ b₂ < ⊤
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- **Alias** of `MulHom.domRestrict`.

---

Restriction of a semigroup hom to a subsemigroup of the domain.  -/
MulHom.restrict : {M : Type u_1} →
  {σ : Type u_4} →
    [inst : Mul M] →
      {N : Type u_5} →
        [inst_1 : Mul N] → [inst_2 : SetLike σ M] → [inst_3 : MulMemClass σ M] → (M →ₙ* N) → (S : σ) → ↥S →ₙ* N
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOn.div` -/
TendstoUniformlyOn.fun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s →
    TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (fun i i_1 => f i i_1 / f' i i_1) (fun i => g i / g' i) l s
-- Init.Data.BitVec.Bitblast
BitVec.carry_zero : ∀ {w : ℕ} {x y : BitVec w} {c : Bool}, BitVec.carry 0 x y c = c
-- Mathlib.Data.Rat.Defs
Rat.addMonoid : AddMonoid ℚ
-- Mathlib.Data.List.MinMax
List.maximum_append : ∀ {α : Type u_1} [inst : LinearOrder α] (l₁ l₂ : List α), (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_closedEBall_comm`. -/
EMetric.mem_closedBall_comm : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal},
  x ∈ Metric.closedEBall y ε ↔ y ∈ Metric.closedEBall x ε
-- Init.Data.Array.Lemmas
Array.flatten_map_toArray : ∀ {α : Type u_1} {L : List (List α)}, (Array.map List.toArray L.toArray).flatten = L.flatten.toArray
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.proved : Lean.Meta.Simp.DischargeResult
-- Mathlib.Topology.ContinuousMap.Sigma
/-- Every continuous map from a connected topological space to the disjoint union of a family of
topological spaces is a composition of the embedding `ContinuousMap.sigmaMk i : C(Y i, Σ i, Y i)`
for some `i` and a continuous map `g : C(X, Y i)`. See also `Continuous.exists_lift_sigma` for a
version with unbundled functions and `ContinuousMap.sigmaCodHomeomorph` for a homeomorphism defined
using this fact.  -/
ContinuousMap.exists_lift_sigma : ∀ {X : Type u_1} {ι : Type u_2} {Y : ι → Type u_3} [inst : TopologicalSpace X]
  [inst_1 : (i : ι) → TopologicalSpace (Y i)] [ConnectedSpace X] (f : C(X, (i : ι) × Y i)),
  ∃ i g, f = (ContinuousMap.sigmaMk i).comp g
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- Notation for the forward direction morphism of the canonical left distributivity isomorphism  -/
CategoryTheory.Distributive.«term∂L» : Lean.ParserDescr
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.instHopfAlgebra : {R : Type u} → [inst : CommRing R] → (self : HopfAlgCat R) → HopfAlgebra R self.carrier
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.unitOfList_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {k : α}, Std.DHashMap.Raw.Const.unitOfList [k] = ∅.insertIfNew k ()
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_dual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L),
  FractionalIdeal.dual A K (FractionalIdeal.dual A K I) = I
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a subtraction monoid under pointwise operations if `α` is.  -/
Set.subtractionMonoid : {α : Type u_2} → [SubtractionMonoid α] → SubtractionMonoid (Set α)
-- Mathlib.RingTheory.TensorProduct.Free
Module.Basis.baseChange_end : ∀ {R : Type u_1} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (A : Type u_5) [inst_4 : CommSemiring A] [inst_5 : Algebra R A] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι R M) (ij : ι × ι), LinearMap.baseChange A (b.end ij) = (Algebra.TensorProduct.basis A b).end ij
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
/-- The forgetful functor `CommMonCat.{u} ⥤ Type u` is corepresentable.  -/
CommMonCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (CommMonCat.of (ULift.{u, 0} (Multiplicative ℕ)))) ≅
  CategoryTheory.forget CommMonCat
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_xor : ∀ {w x y : ℕ}, BitVec.ofNat w (x ^^^ y) = BitVec.ofNat w x ^^^ BitVec.ofNat w y
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.trim_eq_self : ∀ {α : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {n : MeasurableSpace α}
  {v : MeasureTheory.VectorMeasure α M}, v.trim ⋯ = v
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {v w : V} (h : M.IsMatching) (hvw : M.Adj v w),
  h.toEdge ⟨v, ⋯⟩ = ⟨s(v, w), hvw⟩
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson_eq_bot_of_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂),
  Function.Injective ⇑f → Module.jacobson R₂ M₂ = ⊥ → Module.jacobson R M = ⊥
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.mk.sizeOf_spec : ∀ (visitedLevel : Lean.LevelSet) (visitedExpr : Lean.ExprSet) (result : Array Lean.LMVarId),
  sizeOf { visitedLevel := visitedLevel, visitedExpr := visitedExpr, result := result } =
    1 + sizeOf visitedLevel + sizeOf visitedExpr + sizeOf result
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- The infinite product `q ↦ ∏' n, (1 - q^(n+1))` is differentiable on the open unit disc.  -/
ModularForm.differentiableOn_tprod_one_sub_pow : DifferentiableOn ℂ (fun q => ∏' (n : ℕ), (1 - q ^ (n + 1))) (Metric.ball 0 1)
-- Lean.Meta.Closure
/-- Similar to `mkAuxDefinition`, but infers the type of `value`.  -/
Lean.Meta.mkAuxDefinitionFor : Lean.Name → Lean.Expr → optParam Bool false → optParam Bool true → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasCountableProducts_of_hasProducts : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasProducts C],
  CategoryTheory.Limits.HasCountableProducts C
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
`f` is a monotone function on `D`.  -/
monotoneOn_of_hasDerivWithinAt_nonneg : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) → (∀ x ∈ interior D, 0 ≤ f' x) → MonotoneOn f D
-- Init.Prelude
/-- `` `interpolatedStrLitKind `` is the node kind of interpolated string literal
fragments like `"value = {` and `}"` in `s!"value = {x}"`.
 -/
Lean.interpolatedStrLitKind : Lean.SyntaxNodeKind
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.alt.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {ctorName : Lean.Name} {params : Array (Lean.Compiler.LCNF.Param pu)}
  {code : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_1} {ctorName_1 : Lean.Name}
  {params_1 : Array (Lean.Compiler.LCNF.Param pu)} {code_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_1},
  Lean.Compiler.LCNF.Alt.alt ctorName params code h = Lean.Compiler.LCNF.Alt.alt ctorName_1 params_1 code_1 h_1 →
    ctorName = ctorName_1 ∧ params = params_1 ∧ code = code_1
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.Functor.mapHomotopyCategory_obj : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] (c : ComplexShape ι)
  (a : CategoryTheory.Quotient (homotopic V c)),
  (F.mapHomotopyCategory c).obj a = (HomotopyCategory.quotient W c).obj ((F.mapHomologicalComplex c).obj a.as)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖₊ ^ (1 / n)`.  -/
spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] (a : A),
  Filter.Tendsto (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))
-- Mathlib.LinearAlgebra.Semisimple
/-- A linear endomorphism of an `R`-module `M` is called *semisimple* if the induced `R[X]`-module
structure on `M` is semisimple. This is equivalent to saying that every `f`-invariant `R`-submodule
of `M` has an `f`-invariant complement: see `Module.End.isSemisimple_iff`.  -/
Module.End.IsSemisimple : {R : Type u_1} →
  {M : Type u_2} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.Limits.MultispanShape}
  [inst_1 : Unique J.L] {I : CategoryTheory.Limits.MultispanIndex J C} (h : {J.fst default, J.snd default} = Set.univ)
  (h' : J.fst default ≠ J.snd default) (s : CategoryTheory.Limits.PushoutCocone (I.fst default) (I.snd default)),
  (CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork h h' s).π (J.snd default) = s.inr
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
CategoryTheory.Bicategory.isLeftAdjoint_TFAE : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  [CategoryTheory.Bicategory.IsLeftAdjoint f,
      CategoryTheory.Bicategory.HasAbsLeftKanExtension f (CategoryTheory.CategoryStruct.id a),
      ∃ (x : CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.id a)),
        CategoryTheory.Bicategory.Lan.CommuteWith f (CategoryTheory.CategoryStruct.id a) f].TFAE
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk_comp_ofMkLE_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (Y : CategoryTheory.Subobject B) (h₁ : X ≤ CategoryTheory.Subobject.mk f)
  (h₂ : CategoryTheory.Subobject.mk f ≤ Y) {Z : C} (h : CategoryTheory.Subobject.underlying.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f Y h₂) h) =
    CategoryTheory.CategoryStruct.comp (X.ofLE Y ⋯) h
-- Mathlib.Data.Num.Basic
/-- Converts a `Nat` to a `Num`.  -/
Num.ofNat' : ℕ → Num
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instCommMonoid : {α : Type u_1} → [CommMonoid α] → CommMonoid αᵃᵒᵖ
-- Mathlib.Data.Vector.Basic
List.Vector.reverse_reverse : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α n}, v.reverse.reverse = v
-- Init.Data.Vector.Zip
Vector.map_fst_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} (as : Vector α n) {bs : Vector β n}, Vector.map Prod.fst (as.zip bs) = as
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_eq_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} {f : ι → M},
  (∀ i ∈ s, f i = 0) → (s.expect fun i => f i) = 0
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
/-- We say `f` is bounded at `c` if, for all `g` with `g • ∞ = c`, the function `f ∣[k] g` is
bounded at `∞`.  -/
OnePoint.IsBoundedAt : OnePoint ℝ → (UpperHalfPlane → ℂ) → ℤ → Prop
-- Mathlib.RingTheory.Derivation.Basic
Derivation.zero_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (a : A), 0 a = 0
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.candidatesBOfCandidates_mem : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [inst_2 : CompactSpace X]
  [inst_3 : CompactSpace Y] (f : GromovHausdorff.ProdSpaceFun✝ X Y) (fA : f ∈ GromovHausdorff.candidates X Y),
  GromovHausdorff.candidatesBOfCandidates f fA ∈ GromovHausdorff.candidatesB✝ X Y
-- Mathlib.Topology.Connected.Basic
/-- The connected component of `x` in a product space is the product of the connected components
of its coordinates.  -/
connectedComponent_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i),
  connectedComponent x = Set.univ.pi fun i => connectedComponent (x i)
-- ProofWidgets.Cancellable
ProofWidgets.RequestId : Type
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The differential on the complex of morphisms between cochain complexes.  -/
CochainComplex.HomComplex.δ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (n m : ℤ) → CochainComplex.HomComplex.Cochain F G n → CochainComplex.HomComplex.Cochain F G m
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblY_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.dblY P = W.dblU P
-- Mathlib.Algebra.Category.Grp.Limits
/-- A choice of limit cone for a functor into `AddCommGrpCat`.
(Generally, you'll just want to use `limit F`.)  -/
AddCommGrpCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] → CategoryTheory.Limits.Cone F
-- Init.Data.List.Lex
List.lex_eq_decide_lex : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] [inst_2 : DecidableEq α] (lt : α → α → Bool),
  l₁.lex l₂ lt = decide (List.Lex (fun x y => lt x y = true) l₁ l₂)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
RCLike.instContinuousMapUniqueHom : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace A] [T2Space A] [inst_3 : Ring A]
  [inst_4 : StarRing A] [inst_5 : Algebra 𝕜 A], ContinuousMap.UniqueHom 𝕜 A
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.cartan_sup_iSup_rootSpace_eq_top : ∀ {L : Type u_2} [inst : LieRing L] {K : Type u_4} [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L],
  H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieAlgebra.rootSpace H ⇑α = ⊤
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constSMul_apply : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : IsIsometricSMul G X] (c : G) (x : X), (IsometryEquiv.constSMul c) x = c • x
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mk_eq_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {w₁ w₂ : FreeAddMonoid (M ⊕ N)},
  AddMonoid.Coprod.mk w₁ = AddMonoid.Coprod.mk w₂ ↔ (AddMonoid.coprodCon M N) w₁ w₂
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.int.inj : ∀ {i i_1 : ℤ}, Lean.Lsp.DiagnosticCode.int i = Lean.Lsp.DiagnosticCode.int i_1 → i = i_1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_add_mul₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Add β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i + f j) (f k + f l) μ
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.isCompact_preimage : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} [inst_2 : TopologicalSpace β]
  {K : Set β}, HasCompactSupport f → Continuous f → IsClosed K → 0 ∉ K → IsCompact (f ⁻¹' K)
-- Mathlib.Algebra.Polynomial.CancelLeads
Polynomial.neg_cancelLeads : ∀ {R : Type u_1} [inst : Ring R] {p q : Polynomial R}, -p.cancelLeads q = q.cancelLeads p
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.le_degrees_add_right : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  Disjoint p.degrees q.degrees → q.degrees ≤ (p + q).degrees
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.instInfSet : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → InfSet (Submodule R M)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} [inst_3 : AddZeroClass A],
  s.Nonempty → (∀ i ∈ s, f i ≠ 0) → Set.InjOn (AddMonoidAlgebra.supDegree D ∘ f) ↑s → ∑ i ∈ s, f i ≠ 0
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- Qualitative consequence of `logCounting_single_eq_log_sub_const`. The constant function `1 : ℝ → ℝ`
is little o of the logarithmic counting function attached to `single e`.
 -/
Function.locallyFinsuppWithin.one_isLittleO_logCounting_single : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : DecidableEq E] [inst_2 : ProperSpace E] {e : E},
  1 =o[Filter.atTop] Function.locallyFinsuppWithin.logCounting (Function.locallyFinsuppWithin.single e 1)
-- Mathlib.Algebra.Group.Defs
SubtractionMonoid.neg_add_rev : ∀ {G : Type u} [self : SubtractionMonoid G] (a b : G), -(a + b) = -b + -a
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat.add_eq_of_lt : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
  q + r ≠ 0 → q ≠ 0 → r ≠ 0 → padicValRat p q < padicValRat p r → padicValRat p (q + r) = padicValRat p q
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_compl : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (t : Set Ω),
  s.Finite → s.Nonempty → (ProbabilityTheory.uniformOn s) t + (ProbabilityTheory.uniformOn s) tᶜ = 1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal_anti_mono : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {s t : Set (ProjectiveSpectrum 𝒜)},
  s ⊆ t → ProjectiveSpectrum.vanishingIdeal t ≤ ProjectiveSpectrum.vanishingIdeal s
-- Mathlib.RingTheory.Algebraic.Pi
/-- This is not an instance as it forms a diamond with `Pi.instSMul`.

See the `instance_diamonds` test for details.  -/
Polynomial.hasSMulPi : (R : Type u_1) → (S : Type u_2) → [inst : Semiring R] → [SMul R S] → SMul (Polynomial R) (R → S)
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_ker : ∀ {G : Type u_1} [inst : AddGroup G] {G' : Type u_3} [inst_1 : AddGroup G'] (f : G →+ G') [Finite ↥f.range],
  f.ker.FiniteIndex
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is strongly co-Cartesian if for
all morphisms `φ' : a ⟶ b'` and all diagrams of the form
```
a --φ--> b        b'
|        |        |
v        v        v
R --f--> S --g--> S'
```
such that `φ'` lifts `f ≫ g`, there exists a lift `χ` of `g` such that `φ' = χ ≫ φ`.  -/
CategoryTheory.Functor.IsStronglyCocartesian : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        CategoryTheory.Functor 𝒳 𝒮 → {R S : 𝒮} → {a b : 𝒳} → (R ⟶ S) → (a ⟶ b) → Prop
-- Init.Data.String.Lemmas.FindPos
String.pos_eq_posGE : ∀ {s : String} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValid s p}, s.pos p h = s.posGE p ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_comap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (S : AddSubsemigroup P)
  (g : N →ₙ+ P) (f : M →ₙ+ N), AddSubsemigroup.comap f (AddSubsemigroup.comap g S) = AddSubsemigroup.comap (g.comp f) S