mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- **Cauchy-Schwarz inequality** for finsets, squared version.  -/
Finset.sum_mul_sq_le_sq_mul_sq : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [ExistsAddOfLE R] (s : Finset ι) (f g : ι → R), (∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2
-- Mathlib.Data.Set.Image
Set.preimage_symmDiff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s t : Set β), f ⁻¹' symmDiff s t = symmDiff (f ⁻¹' s) (f ⁻¹' t)
-- Mathlib.Computability.Partrec
Nat.rfind_min : ∀ {p : ℕ →. Bool} {n : ℕ}, n ∈ Nat.rfind p → ∀ {m : ℕ}, m < n → false ∈ p m
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_sInf : ∀ {α : Type u_1} [inst : LE α] (S : Set (LowerSet α)), (sInf S).compl = ⨅ s ∈ S, s.compl
-- Mathlib.GroupTheory.OrderOfElement
finEquivMultiples_symm_apply : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) (n : ℕ),
  (finEquivMultiples hx).symm ⟨n • x, ⋯⟩ = ⟨n % addOrderOf x, ⋯⟩
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of `Cardinal.sdiff_nonempty_of_mk_lt_mk`. -/
Cardinal.diff_nonempty_of_mk_lt_mk : ∀ {α : Type u} {S T : Set α}, Cardinal.mk ↑S < Cardinal.mk ↑T → (T \ S).Nonempty
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.codeBlock.withIndentColumn : (ℕ → Lean.Parser.ParserFn) → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.lineGraph.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V),
  G.lineGraph = { Adj := fun e₁ e₂ => e₁ ≠ e₂ ∧ (↑↑e₁ ∩ ↑↑e₂).Nonempty, symm := ⋯, loopless := ⋯ }
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimTargetView.mk.inj : ∀ {hIdent? : Option Lean.Ident} {term : Lean.Syntax} {hIdent?_1 : Option Lean.Ident} {term_1 : Lean.Syntax},
  { hIdent? := hIdent?, term := term } = { hIdent? := hIdent?_1, term := term_1 } → hIdent? = hIdent?_1 ∧ term = term_1
-- Mathlib.Analysis.Real.Sqrt
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`.  -/
NNReal.sum_mul_le_sqrt_mul_sqrt : ∀ {ι : Type u_2} (s : Finset ι) (f g : ι → NNReal),
  ∑ i ∈ s, f i * g i ≤ NNReal.sqrt (∑ i ∈ s, f i ^ 2) * NNReal.sqrt (∑ i ∈ s, g i ^ 2)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.measure_sdiff_biUnion : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s),
  μ (s \ ⋃ p ∈ h.index, h.covering p) = 0
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsTheta.trans_isEquivalent : ∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f : α → β₂} {g₁ g₂ : α → β}, f =Θ[l] g₁ → Asymptotics.IsEquivalent l g₁ g₂ → f =Θ[l] g₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- A version of `cfc_eq_cfcL` in terms of `ContinuousMapZero.mkD`  -/
cfc_eq_cfcL_mkD : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring 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] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  (ha : autoParam (p a) _auto_113✝), cfc f a = (cfcL ha) (ContinuousMap.mkD ((spectrum R a).domRestrict f) 0)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_cancel' : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {r₁ : R} {r₂ : X} {s t : ↥S}, (r₁ + ↑s -ₒ t) +ᵥ r₂ -ₒ s = (r₁ +ᵥ r₂) -ₒ t
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coconeOfPreserves_pt_left : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L]
  {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))),
  (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.left = c₁.pt
-- Mathlib.CategoryTheory.Preadditive.Projective.Internal
CategoryTheory.InternallyProjective.preserves_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (P : C) [CategoryTheory.InternallyProjective P],
  (CategoryTheory.ihom P).PreservesEpimorphisms
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonNameMap : {α : Type} → [Lean.ToJson α] → Lean.ToJson (Lean.NameMap α)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
-- Init.Data.Order.Classes
Std.IsPreorder.mk : ∀ {α : Type u} [inst : LE α], (∀ (a : α), a ≤ a) → (∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) → Std.IsPreorder α
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.resetOnStack : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → Lean.SCC.M α Unit
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- A *semisimple* Lie algebra is one that is a direct sum of non-abelian atomic ideals.
These ideals are simple Lie algebras, by `LieAlgebra.IsSemisimple.isSimple_of_isAtom`.

Note that the label 'semisimple' is apparently not universally agreed
[upon](https://mathoverflow.net/questions/149391/on-radicals-of-a-lie-algebra#comment383669_149391)
for general coefficients.

For example [Seligman, page 15](seligman1967) uses the label for `LieAlgebra.HasTrivialRadical`,
the weakest of the various properties which are all equivalent over a field of characteristic zero.
 -/
LieAlgebra.IsSemisimple : (R : Type u_1) → (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop
-- Init.Data.UInt.Basic
/-- Bitwise and for 32-bit unsigned integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.land : UInt32 → UInt32 → UInt32
-- Mathlib.GroupTheory.Index
Subgroup.index_map_of_bijective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Bijective ⇑f → ∀ (H : Subgroup G), (Subgroup.map f H).index = H.index
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport.kind : Lean.Lsp.LeanImport → Lean.Lsp.LeanImportKind
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃Functor_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {X Y : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  (φ : X ⟶ Y), CategoryTheory.bifunctorComp₂₃Functor.map φ = CategoryTheory.bifunctorComp₂₃FunctorMap φ
-- Mathlib.Data.Sum.Basic
Sum.update_inl_apply_inl' : ∀ {α : Type u} {β : Type v} {γ : α ⊕ β → Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)]
  {f : (i : α ⊕ β) → γ i} {i : α} {x : γ (Sum.inl i)} (j : α),
  Function.update f (Sum.inl i) x (Sum.inl j) = Function.update (fun j => f (Sum.inl j)) i x j
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.encard_edgeSet_completeBipartiteGraph : ∀ {W₁ : Type u_2} {W₂ : Type u_3}, (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_left_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).left.K = S.cycles
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_succ_succ_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) self.map = f.map
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] (F : ι → α → β)
  (f : α → β) (p : Filter ι),
  TendstoLocallyUniformly F f p =
    ∀ u ∈ uniformity β, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
GroupLieAlgebra.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4)
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G], GroupLieAlgebra I G = TangentSpace I 1
-- Mathlib.Topology.Maps.Strict.Basic
/-- Homeomorphisms are precisely bijective strict maps.  -/
Topology.isHomeomorph_iff_isStrictMap_bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f ↔ Topology.IsStrictMap f ∧ Function.Bijective f
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- the isomorphism between the homology of the `r`-th page at an object `pq : κ`
and the corresponding object on the next page  -/
CategoryTheory.SpectralSequence.iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            (self : CategoryTheory.SpectralSequence C c r₀) →
              (r r' : ℤ) →
                (pq : κ) →
                  (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
                    (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) →
                      (self.page r ⋯).homology pq ≅ (self.page r' ⋯).X pq
-- Mathlib.Util.Export
Lean.Export.State.levels : Lean.Export.State → Lean.Export.Alloc Lean.Level
-- Mathlib.SetTheory.Lists
Lists.instMembership : {α : Type u_1} → Membership (Lists α) (Lists α)
-- Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
PiTensorProduct.ofDirectSumEquiv.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Finite ι], PiTensorProduct.ofDirectSumEquiv = PiTensorProduct.ofDFinsuppEquiv
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.List.getElem?_zipWithAll.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          (Unit → motive none none) →
            ((a? : Option α) → (b? : Option β) → (a? = none → b? = none → False) → motive a? b?) → motive x x_1
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.isBigO_of_div_tendsto_atTop : ∀ {f g : ℝ → ℝ} {l : Filter ℝ}, Filter.Tendsto (fun x => g x / f x) l Filter.atTop → f =O[l] g
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extend_def : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β}, UniformContinuous f → pkg.extend f = ⋯.extend f
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft_sumInr : ∀ {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι'' → Type u_9) (e : ι ⊕ ι' ≃ ι'')
  (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (j : ι'),
  (Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.accept.inj : ∀ {ctx : Type u_1} {context context_1 : ctx},
  Mathlib.TacticAnalysis.TriggerCondition.accept context = Mathlib.TacticAnalysis.TriggerCondition.accept context_1 →
    context = context_1
-- Mathlib.Computability.Primrec.Basic
Primrec.unpair : Primrec Nat.unpair
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {β : Type w'} [inst_2 : LinearOrder β]
  [OrderBot β] [inst_4 : SuccOrder β] [inst_5 : WellFoundedLT β] (b : β),
  P.strictLimitsClosureIter J b ≤ P.limitsClosure J
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_ne : ∀ {α : Type u_1}, Sym2.fromRel ⋯ = {z | ¬z.IsDiag}
-- Init.Data.BitVec.Basic
/-- Returns the `i`th most significant bit, or `false` if `i ≥ w`.  -/
BitVec.getMsbD : {w : ℕ} → BitVec w → ℕ → Bool
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.Hom.opensRange (I.subschemeCover.f U) = (TopologicalSpace.Opens.map I.subschemeι.base).obj ↑U
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The second projection at a point in a product is `C^∞`.  -/
contDiffAt_snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {p : E × F},
  ContDiffAt 𝕜 n Prod.snd p
-- Mathlib.CategoryTheory.Generator.Basic
/-- An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered
category with a small coseparating set has an initial object.

In fact, it follows from the Special Adjoint Functor Theorem that `C` is already cocomplete,
see `hasColimits_of_hasLimits_of_isCoseparating`.  -/
CategoryTheory.hasInitial_of_isCoseparating : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v₁, u₁} C]
  {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} P],
  P.IsCoseparating → CategoryTheory.Limits.HasInitial C
-- Lean.Structure
Lean.StructureInfo.mk.inj : ∀ {structName : Lean.Name} {fieldNames : Array Lean.Name} {fieldInfo : Array Lean.StructureFieldInfo}
  {parentInfo : Array Lean.StructureParentInfo} {structName_1 : Lean.Name} {fieldNames_1 : Array Lean.Name}
  {fieldInfo_1 : Array Lean.StructureFieldInfo} {parentInfo_1 : Array Lean.StructureParentInfo},
  { structName := structName, fieldNames := fieldNames, fieldInfo := fieldInfo, parentInfo := parentInfo } =
      { structName := structName_1, fieldNames := fieldNames_1, fieldInfo := fieldInfo_1, parentInfo := parentInfo_1 } →
    structName = structName_1 ∧ fieldNames = fieldNames_1 ∧ fieldInfo = fieldInfo_1 ∧ parentInfo = parentInfo_1
-- Mathlib.Algebra.Lie.BaseChange
/-- The Lie bracket on the extension of a Lie algebra `L` over `R` by an algebra `A` over `R`.  -/
_private.Mathlib.Algebra.Lie.BaseChange.0.LieAlgebra.ExtendScalars.bracket' : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      (M : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] →
              [inst_3 : LieRing L] →
                [inst_4 : LieAlgebra R L] →
                  [inst_5 : AddCommGroup M] →
                    [inst_6 : Module R M] →
                      [inst_7 : LieRingModule L M] →
                        [LieModule R L M] → TensorProduct R A L →ₗ[A] TensorProduct R A M →ₗ[A] TensorProduct R A M
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (ff : f ⟶ g)
  [CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.left ff)] [CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.right ff)],
  CategoryTheory.IsIso ff
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.rpow_logb_eq_abs : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → x ≠ 0 → b ^ Real.logb b x = |x|
-- Mathlib.Algebra.GCDMonoid.Nat
Int.associated_iff_natAbs : ∀ {a b : ℤ}, Associated a b ↔ a.natAbs = b.natAbs
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instHomIsOverId : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : C) [inst_1 : CategoryTheory.OverClass X S],
  CategoryTheory.HomIsOver (CategoryTheory.CategoryStruct.id X) S
-- Mathlib.CategoryTheory.Action.Monoidal
Action.forget_η : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  CategoryTheory.Functor.OplaxMonoidal.η (Action.forget V G) =
    CategoryTheory.CategoryStruct.id
      ((Action.forget V G).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)))
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.apply_smulCommClass : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] {S : Type u_1}
  [inst_3 : SMul S R] [inst_4 : SMul S A₁] [IsScalarTower S R A₁], SMulCommClass S (A₁ ≃ₐ[R] A₁) A₁
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_filter_key : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool} {k : α},
  k ∈ Std.ExtDHashMap.filter (fun a x => f a) m ↔ ∃ (h : k ∈ m), f (m.getKey k h) = true
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- A nonsingular point on a Weierstrass curve `W` in affine coordinates. This is either the unique
point at infinity `WeierstrassCurve.Affine.Point.zero` or a nonsingular affine point
`WeierstrassCurve.Affine.Point.some (x, y)` satisfying the Weierstrass equation of `W`.  -/
WeierstrassCurve.Affine.Point : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → Type r
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C}
  (h_1 : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h)
      (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h_1) =
    CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i.1 i.2 i₁₂') h_1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.subset_zero : ∀ {α : Type u_1} {s : Multiset α}, s ⊆ 0 ↔ s = 0
-- Lean.Declaration
Lean.instBEqOpaqueVal : BEq Lean.OpaqueVal
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr'_ι : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
  (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx)
  (n : N) (m : M), (CliffordAlgebra.foldr' Q f hf n) ((CliffordAlgebra.ι Q) m) = (f m) (1, n)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to negative infinity along a filter, then `f` multiplied by
a positive constant (on the right) also tends to negative infinity.  -/
Filter.Tendsto.atBot_mul_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atBot
-- Mathlib.Analysis.InnerProductSpace.l2Space
lp.hasSum_inner : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : ι → Type u_4} [inst_1 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_2 : (i : ι) → InnerProductSpace 𝕜 (G i)] (f g : ↥(lp G 2)),
  HasSum (fun i => inner 𝕜 (↑f i) (↑g i)) (inner 𝕜 f g)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : BoundedOrder α] →
          [inst_3 : BoundedOrder β] →
            (toOrderHom : α →o β) → toOrderHom.toFun ⊤ = ⊤ → toOrderHom.toFun ⊥ = ⊥ → BoundedOrderHom α β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α} {fallback : γ},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.map f m) k fallback =
        (Option.map (f k') (Std.DHashMap.Raw.Const.get? m k)).getD fallback
-- Mathlib.Algebra.Torsor.Basic
Function.Injective.addTorsor.eq_1 : ∀ {G : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : AddGroup G] [inst_1 : AddTorsor G P] [inst_2 : VAdd G Q]
  [inst_3 : VSub G Q] [inst_4 : Nonempty Q] (f : Q → P) (hf : Function.Injective f)
  (smul : ∀ (c : G) (x : Q), f (c +ᵥ x) = c +ᵥ f x) (sdiv : ∀ (x y : Q), x -ᵥ y = f x -ᵥ f y),
  Function.Injective.addTorsor f hf smul sdiv =
    { toAddAction := Function.Injective.addAction f hf smul, toVSub := inst_3, nonempty := inst_4, vsub_vadd' := ⋯,
      vadd_vsub' := ⋯ }
-- Mathlib.Data.PFun
PFun.prodMap_comp_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ι : Type u_6} (f₁ : α →. β) (f₂ : β →. γ)
  (g₁ : δ →. ε) (g₂ : ε →. ι), (f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)
-- Std.Http.Data.Headers.Basic
/-- Serializes the typed representation back to a name-value pair.
 -/
Std.Http.Header.serialize : {α : Type} → [self : Std.Http.Header α] → α → Std.Http.Header.Name × Std.Http.Header.Value
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  P = Q → W'.add P Q = W'.dblXYZ P
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_ε : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.AddMon.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Y`-coordinate of a representative of `-(2 • P)` for a projective point representative `P`
on a Weierstrass curve.  -/
WeierstrassCurve.Projective.negDblY : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → R