mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- **Unconditional summation**: a function on `β` is said to be *unconditionally summable* if its
partial sums over finite subsets converge with respect to the `atTop` filter.  -/
SummationFilter.unconditional : (β : Type u_2) → SummationFilter β
-- Lean.Meta.Tactic.Simp.SimpAll
_private.Lean.Meta.Tactic.Simp.SimpAll.0.Lean.Meta.SimpAll.loop : Lean.Meta.SimpAll.M Bool
-- Mathlib.Data.Finsupp.Notation
Finsupp.fun₀.matchAlts.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.snd_comp_prod : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (f : A →A[R] B)
  (g : A →A[R] C), (ContinuousAlgHom.snd R B C).comp (f.prod g) = g
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.of_mono_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [CategoryTheory.Mono 0], CategoryTheory.Limits.IsZero X
-- Mathlib.LinearAlgebra.Ray
/-- A nonnegative multiple of a vector is in the same ray as one it is in the same ray as.  -/
SameRay.nonneg_smul_left : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M} {S : Type u_5} [inst_5 : CommSemiring S]
  [inst_6 : PartialOrder S] [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M]
  {a : S}, SameRay R x y → 0 ≤ a → SameRay R (a • x) y
-- Mathlib.Order.Filter.Map
Function.RightInverse.filter_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.RightInverse g f → Function.LeftInverse (Filter.comap g) (Filter.comap f)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_lie : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f g : Module.End R M), (LinearMap.trace R M) ⁅f, g⁆ = 0
-- Init.Core
/-- Non-instance for `DecidableEq` from `LawfulBEq`.
To use this, add `attribute [local instance 5] instDecidableEqOfLawfulBEq` at the top of a file.
 -/
instDecidableEqOfLawfulBEq : {α : Type u_1} → [inst : BEq α] → [LawfulBEq α] → DecidableEq α
-- Lean.DocString.Markdown
/-- Drops trailing ASCII spaces (`' '`) from a string. Used to compute the "empty line" form of a
per-line prefix (`"> "` becomes `">"`) so that prefixed empty lines don't carry trailing whitespace
into the rendered output.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.trimEndSpaces : String → String
-- Mathlib.Order.KrullDimension
Order.KrullDimLE.mono : ∀ {n m : ℕ}, n ≤ m → ∀ (α : Type u_1) [inst : Preorder α] [Order.KrullDimLE n α], Order.KrullDimLE m α
-- Init.Data.SInt.Bitwise
Int16.ofBitVec_intMax : Int16.ofBitVec (BitVec.intMax 16) = Int16.maxValue
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey? =
    some (t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k')
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = t.isEmpty
-- Mathlib.Tactic.Simps.NotationClass
Simps.instInhabitedAutomaticProjectionData : Inhabited Simps.AutomaticProjectionData
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- For any left ideal $I ≤ R$, we have $Mₙ(J(I)) ≤ J(Mₙ(I))$.  -/
Ideal.matrix_jacobson_le : ∀ {R : Type u_1} [inst : Ring R] {n : Type u_2} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : Ideal R),
  Ideal.matrix n I.jacobson ≤ (Ideal.matrix n I).jacobson
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.subsumes_right : ∀ (f f₁ f₂ : Sat.Fmla), f.subsumes (f₁.and f₂) → f.subsumes f₂
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- **Alias** of `MeasureTheory.ae_eq_set_sdiff`. -/
MeasureTheory.ae_eq_set_diff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s =ᵐ[μ] t → s' =ᵐ[μ] t' → s \ s' =ᵐ[μ] t \ t'
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.HasExt C]
  (K L : CochainComplex C ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE a] [L.IsGE b] [L.IsLE b],
  CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
-- Lean.Meta.Match.MatcherApp.Transform
Lean.Meta.MatcherApp.TransformAltFVars.mk.injEq : ∀ (args fields overlaps discrEqs extraEqs args_1 fields_1 overlaps_1 discrEqs_1 extraEqs_1 : Array Lean.Expr),
  ({ args := args, fields := fields, overlaps := overlaps, discrEqs := discrEqs, extraEqs := extraEqs } =
      { args := args_1, fields := fields_1, overlaps := overlaps_1, discrEqs := discrEqs_1, extraEqs := extraEqs_1 }) =
    (args = args_1 ∧ fields = fields_1 ∧ overlaps = overlaps_1 ∧ discrEqs = discrEqs_1 ∧ extraEqs = extraEqs_1)
-- Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
QuadraticMap.lineDifferentiableAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : QuadraticMap 𝕜 E F) (a b : E),
  LineDifferentiableAt 𝕜 (⇑f) a b
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.mul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸} {c' : 𝔸},
  HasDerivWithinAt c c' s x → ∀ (d : 𝔸), HasDerivWithinAt (fun y => c y * d) (c' * d) s x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Construct a functor out of the wide pullback shape given a J-indexed collection of arrows to a
fixed object.
 -/
CategoryTheory.Limits.WidePullbackShape.wideCospan : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (objs : J → C) → ((j : J) → objs j ⟶ B) → CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C
-- Lean.Environment
_private.Lean.Environment.0.Lean.importModulesCore.loadIR : Lean.NameMap Lean.ImportArtifacts → Lean.Import → Lean.ImportStateM (Array (Lean.ModuleData × Lean.CompactedRegion))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_le_of_one_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b c : α},
  b ≤ c → 1 < a → b < c * a
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_spec : ∀ (n : ℕ), ∑ k ∈ Finset.range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k = 1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry.mk.sizeOf_spec : ∀ (waiters : Array Lean.Meta.SynthInstance.Waiter) (answers : Array Lean.Meta.SynthInstance.Answer),
  sizeOf { waiters := waiters, answers := answers } = 1 + sizeOf waiters + sizeOf answers
-- Mathlib.RingTheory.Finiteness.Nilpotent
Matrix.isNilpotent_transpose_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {A : Matrix ι ι R}, IsNilpotent A.transpose ↔ IsNilpotent A
-- Init.Data.String.Basic
String.Pos.Raw.isValid.fun_cases_unfolding : ∀ (s : String) (p : String.Pos.Raw) (motive : Bool → Prop),
  (∀ (h : p < s.rawEndPos), motive (decide (s.getUTF8Byte p h).IsUTF8FirstByte)) →
    (¬p < s.rawEndPos → motive (decide (p = s.rawEndPos))) → motive (String.Pos.Raw.isValid s p)
-- Mathlib.Algebra.Free
FreeMagma.lift_of : ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : α → β) (x : α), (FreeMagma.lift f) (FreeMagma.of x) = f x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_map_fst_of_containsKey_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValue? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instContinuousEval : ∀ {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 : ℕ∞}, ContinuousEval (TestFunction Ω F n) E F
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_of_right : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ g → s ∈ f ⊓ g
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_le : ∀ {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] {S : NonUnitalSubalgebra R A} {s : Set A},
  s ⊆ ↑S → NonUnitalAlgebra.adjoin R s ≤ S
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.instNonempty : ∀ (M : Type u_1) [inst : Monoid M] (X : Type u) [inst_1 : MulAction M X] [Nonempty X],
  Nonempty (CategoryTheory.ActionCategory M X)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instDistribMulActionOfReal : {R : Type u_1} → [inst : Semiring R] → [DistribMulAction R ℝ] → DistribMulAction R ℂ
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.SearchState.mk.sizeOf_spec : ∀ (choiceStack : List Lean.Meta.Grind.EMatch.Choice) (instanceMap : Lean.Meta.Grind.EMatch.InstanceMap),
  sizeOf { choiceStack := choiceStack, instanceMap := instanceMap } = 1 + sizeOf choiceStack + sizeOf instanceMap
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.name : Lean.Lsp.LeanModule → String
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv.instIsMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivisionMonoid G] [MeasurableMul G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant], μ.inv.IsMulLeftInvariant
-- Mathlib.Topology.Bornology.BoundedOperation
tendsto_const_sub_cobounded : ∀ {R : Type u_1} [inst : SeminormedAddCommGroup R] (x : R),
  Filter.Tendsto (fun x_1 => x - x_1) (Bornology.cobounded R) (Bornology.cobounded R)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ofCone_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cone F)
  (j : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.Trident.ofCone t).π.app j =
    CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedLevelMVarErrorInfo.default : Lean.Elab.Term.LevelMVarErrorInfo
-- Qq.Macro
Qq.Impl.lctxHasMVar : Lean.MetaM Bool
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_inter_eq_size_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
/-- The integral of `f (R • x)` with respect to an additive Haar measure is a multiple of the
integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
thanks to the convention that a non-integrable function has integral zero.  -/
MeasureTheory.Measure.integral_comp_smul_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] (f : E → F) (R : ℝ) {hR : 0 ≤ R},
  ∫ (x : E), f (R • x) ∂μ = (R ^ Module.finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
-- Batteries.Data.ByteSlice
ByteSlice.instStreamUInt8_batteries : Std.Stream ByteSlice UInt8
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), Function.Surjective ⇑f
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : Set α}, IsOpen U → IsOpen {s | (s ∩ U).Nonempty}
-- Mathlib.RingTheory.Ideal.Maps
Ideal.relIsoOfBijective.congr_simp : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  (f f_1 : F) (e_f : f = f_1) [inst_3 : RingHomClass F R S] (hf : Function.Bijective ⇑f),
  Ideal.relIsoOfBijective f hf = Ideal.relIsoOfBijective f_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Naturality of the oplax naturality constraint.  -/
CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.OplaxTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g)
  {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (self.app a) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (CategoryTheory.CategoryStruct.comp (self.naturality g) h) =
    CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.support_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], SkewMonoidAlgebra.support 0 = ∅
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.one_lt_dist_of_ne_of_not_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Connected → u ≠ v → ¬G.Adj u v → 1 < G.dist u v
-- Std.Data.ExtDTreeMap.Basic
/-- Returns an array of all keys present in the tree map in ascending  order.  -/
Std.ExtDTreeMap.keysArray : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Array α
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_of_forall_pos_le_add : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α]
  {a b : α}, (∀ (ε : α), 0 < ε → a ≤ b + ε) → a ≤ b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_id : ∀ {α : Type u_5} [inst : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {x : MeasurableSpace α}
  [OpensMeasurableSpace α] [SecondCountableTopology α] {μ : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable id μ
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_iSup₂_iff : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {a : α} {f : (i : ι) → κ i → UpperSet α},
  a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
-- Mathlib.Algebra.Order.Group.PiLex
Pi.Lex.isOrderedCancelMonoid : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CommMonoid (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelMonoid (α i)],
  IsOrderedCancelMonoid (Lex ((i : ι) → α i))
-- Mathlib.Algebra.Lie.Abelian
LieModule.ker.congr_simp : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.ker R L M = LieModule.ker R L M
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_odd : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.preΨ (2 * m + 1) =
    (W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
      W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2
-- Lean.Environment
Lean.AsyncConstantInfo.toConstantInfo : Lean.AsyncConstantInfo → Lean.ConstantInfo
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.modifyTR.go.eq_2 : ∀ {α : Type u_1} (f : α → α) (a : Array α) (head : α) (xs : List α),
  List.modifyTR.go✝ f (head :: xs) 0 a = a.toListAppend (f head :: xs)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value is positive definitive  -/
IsAbsoluteValue.abv_eq_zero' : ∀ {S : Type u_5} {inst : Semiring S} {inst_1 : PartialOrder S} {R : Type u_6} {inst_2 : Semiring R} {f : R → S}
  [self : IsAbsoluteValue f] {x : R}, f x = 0 ↔ x = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → W.addXYZ P Q = WeierstrassCurve.Projective.addU P Q • ![0, 1, 0]
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_add_union_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
_private.Mathlib.RingTheory.Extension.Presentation.Submersive.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_inl_inr : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Fintype σ] [inst_8 : Fintype σ'] (i : σ') (j : σ),
  (Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inr j) = 0
-- Lean.Elab.DeprecatedArg
/-- Entry mapping an old parameter name to a new (or no) parameter for a given declaration.  -/
Lean.Elab.DeprecatedArgEntry : Type
-- Init.Data.Array.Lemmas
/-- Variant of `allM_toArray` with a side condition on `stop`.  -/
List.allM_toArray' : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} {stop : ℕ},
  stop = l.toArray.size → Array.allM p l.toArray 0 stop = List.allM p l
-- Mathlib.Order.CompleteBooleanAlgebra
Prop.instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Prop
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.vsub_toAffineMap : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] (f g : P →ᴬ[R] Q), ↑(f -ᵥ g) = ↑f -ᵥ ↑g
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- `adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`.  -/
IntermediateField.adjoin : (F : Type u_1) →
  [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → Set E → IntermediateField F E
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.rTensor_reflects_triviality : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FaithfullyFlat R M] (N : Type u_1) [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [h : Subsingleton (TensorProduct R N M)], Subsingleton N
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_ε_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal] {Z : C}
  (h : (F.obj n).obj ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((CategoryTheory.Functor.LaxMonoidal.ε F).app X)) h =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor n).inv).app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) n).app X) h)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.instAB4StarOfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  [CategoryTheory.AB4StarOfSize.{w, v, u} C], CategoryTheory.AB4StarOfSize.{0, v, u} C
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds : ∀ {Ω : Type u_1} [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (P : MeasureTheory.ProbabilityMeasure Ω) {G : Set Ω},
  IsOpen G → ∀ {ε : ENNReal}, 0 < ε → {Q | ↑P G < ↑Q G + ε} ∈ nhds P
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.one_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M), 1 x = x
-- Lean.Server.References
Lean.Server.instFromJsonIlean.fromJson : Lean.Json → Except String Lean.Server.Ilean
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.leftAdjointSquare.vcomp.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d}
  {h₂ : d ⟶ f} {l₁ : a ⟶ b} {l₂ : c ⟶ d} {l₃ : e ⟶ f}
  (α : CategoryTheory.CategoryStruct.comp g₁ l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp g₂ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h₂),
  CategoryTheory.Bicategory.leftAdjointSquare.vcomp α β =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator g₁ g₂ l₃).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g₁ β)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator g₁ l₂ h₂).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight α h₂)
            (CategoryTheory.Bicategory.associator l₁ h₁ h₂).hom)))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_diff_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
inv_riemannZeta_isBigO : (fun s => (riemannZeta s)⁻¹) =O[nhdsWithin 1 {1}ᶜ] fun x => x - 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- Bundle `cfc f a` into a unit given a proof that `f` is nonzero on the spectrum of `a`.  -/
cfcUnits : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : Semifield R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : TopologicalSpace A] →
                  [inst_6 : Ring A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : Algebra R A] →
                        [ContinuousFunctionalCalculus R A p] →
                          [ContinuousInv₀ R] →
                            (f : R → R) →
                              (a : A) →
                                (∀ x ∈ spectrum R a, f x ≠ 0) →
                                  autoParam (ContinuousOn f (spectrum R a)) cfcUnits._auto_1 →
                                    autoParam (p a) cfcUnits._auto_3 → Aˣ
-- Mathlib.Order.Ideal
/-- **Alias** of the forward direction of `Order.Ideal.top_mem_iff_eq_top`. -/
Order.Ideal.top_of_top_mem : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderTop P] {I : Order.Ideal P}, ⊤ ∈ I → I = ⊤
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_succ' : ∀ {n d : ℕ} (a : Fin (n + 1) → ℕ), (Behrend.map d) a = a 0 + (Behrend.map d) (a ∘ Fin.succ) * d