mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Turn a morphism in `SemimoduleCat` back into a `LinearMap`.  -/
SemimoduleCat.Hom.hom : {R : Type u} → [inst : Semiring R] → {A B : SemimoduleCat R} → A.Hom B → ↑A →ₗ[R] ↑B
-- Init.Data.Option.Lemmas
Option.getD_choice : ∀ {α : Type u_1} {a : α}, (Option.choice α).getD a = (Option.choice α).get ⋯
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.hull_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} {ι : Sort v} (s : ι → α),
  PrimitiveSpectrum.hull T (iSup s) = ⋂ i, PrimitiveSpectrum.hull T (s i)
-- Batteries.Data.AssocList
Batteries.AssocList.empty_eq : ∀ {α : Type u_1} {β : Type u_2}, ∅ = Batteries.AssocList.nil
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.commAlgEquiv_X : ∀ {R : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [inst : CommSemiring R] (i : S₁),
  (MvPolynomial.commAlgEquiv R S₁ S₂) (MvPolynomial.X i) = MvPolynomial.C (MvPolynomial.X i)
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Lean.Meta.Grind.Origin.fvar fvarId = Lean.Meta.Grind.Origin.fvar fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.ext : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {f g : P →ᵃⁱ[𝕜] P₂}, (∀ (x : P), f x = g x) → f = g
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_comm : ∀ {α : Type u_3} [inst : DivisionRing α] (r : ℚ) (a : α), ↑r * a = a * ↑r
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f g : β → α}, (∀ (b : β), f b = g b) → ∑'[L] (b : β), f b = ∑'[L] (b : β), g b
-- Init.Grind.Interactive
/-- `next => tac` focuses on the next goal and solves it using `tac`, or else fails.
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
inaccessible names to the given names.
 -/
Lean.Parser.Tactic.Grind.next : Lean.ParserDescr
-- Mathlib.Order.Hom.Basic
/-- The composition of two bundled monotone functions, a fully bundled version.  -/
OrderHom.compₘ : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Preorder γ] → (β →o γ) →o (α →o β) →o α →o γ
-- Init.Data.List.Sublist
List.suffix_cons_iff : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.rfl : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G ≤s G
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
CFC.tendsto_cfc_rpow_sub_one_log : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  autoParam (IsStrictlyPositive a) CFC.tendsto_cfc_rpow_sub_one_log._auto_1 →
    Filter.Tendsto (fun p => cfc (fun x => p⁻¹ * (x ^ p - 1)) a) (nhdsWithin 0 (Set.Ioi 0)) (nhds (CFC.log a))
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- A property satisfied almost everywhere is satisfied on a dense subset.  -/
MeasureTheory.Measure.dense_of_ae : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {p : X → Prop}, (∀ᵐ (x : X) ∂μ, p x) → Dense {x | p x}
-- Mathlib.LinearAlgebra.Matrix.Block
/-- **Alias** of `Matrix.det_of_isLowerTriangular`. -/
Matrix.det_of_lowerTriangular : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : LinearOrder m]
  (M : Matrix m m R), M.IsLowerTriangular → M.det = ∏ i, M i i
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instIsOrderedRing : ∀ {X : AlgebraicGeometry.Scheme}, IsOrderedRing X.IdealSheafData
-- Mathlib.Data.Multiset.Filter
Multiset.filter_subset : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α), Multiset.filter p s ⊆ s
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.brecOn_1.eq : ∀ {m : Type u → Type u} {α : Type u} {motive_1 : MLList.MLListImpl✝ m α → Sort u_1}
  {motive_2 : Thunk (MLList.MLListImpl✝ m α) → Sort u_1} (t : Thunk (MLList.MLListImpl✝ m α))
  (F_1 : (t : MLList.MLListImpl✝ m α) → MLList.MLListImpl.below✝ t → motive_1 t)
  (F_2 : (t : Thunk (MLList.MLListImpl✝ m α)) → MLList.MLListImpl.below_1✝ t → motive_2 t),
  MLList.MLListImpl.brecOn_1✝ t F_1 F_2 = F_2 t (MLList.MLListImpl.brecOn_1.go✝ t F_1 F_2).2
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
/-- The linear map from the `n`th exterior power to the `n`th tensor power obtained by
`MultilinearMap.alternatization`.  -/
exteriorPower.toTensorPower : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (n : ℕ) → ↥(⋀[R]^n M) →ₗ[R] TensorPower R n M
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_differentiableWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G},
  DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductCone_pt_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C),
  (CategoryTheory.FunctorToTypes.binaryProductCone F G).pt.obj a = (F.obj a × G.obj a)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
CommRingCat.KaehlerDifferential.map.congr_simp : ∀ {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g g_1 : A ⟶ A'} (e_g : g = g_1) {g' : B ⟶ B'}
  (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g'),
  CommRingCat.KaehlerDifferential.map fac = CommRingCat.KaehlerDifferential.map ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.norm_mem_spectrum_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] [Nontrivial A] {a : A},
  autoParam (0 ≤ a) CStarAlgebra.norm_mem_spectrum_of_nonneg._auto_1 → ‖a‖ ∈ spectrum ℝ a
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_toUInt16 : ∀ (n : UInt32), n.toUInt16.toUInt8 = n.toUInt8
-- Init.Data.List.Lemmas
List.flatten_replicate_replicate : ∀ {n m : ℕ} {α : Type u_1} {a : α}, (List.replicate n (List.replicate m a)).flatten = List.replicate (n * m) a
-- Lean.Util.MonadCache
Lean.MonadHashMapCacheAdapter.mk : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        m (Std.HashMap α β) → ((Std.HashMap α β → Std.HashMap α β) → m Unit) → Lean.MonadHashMapCacheAdapter α β m
-- Std.Tactic.BVDecide.Reflect
/-- Verify that `cert` is an UNSAT proof for the SAT problem obtained by bitblasting `bv`.
 -/
Std.Tactic.BVDecide.Reflect.verifyBVExpr : Std.Tactic.BVDecide.BVLogicalExpr → String → Bool
-- Mathlib.Probability.Kernel.Disintegration.Density
/-- An `ℕ`-indexed martingale that is a density for `κ` with respect to `ν` on the sets in
`countablePartition γ n`. Used to define its limit `ProbabilityTheory.Kernel.density`, which is
a density for those kernels for all measurable sets.  -/
ProbabilityTheory.Kernel.densityProcess : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} →
            [MeasurableSpace.CountablyGenerated γ] →
              ProbabilityTheory.Kernel α (γ × β) → ProbabilityTheory.Kernel α γ → ℕ → α → γ → Set β → ℝ
-- Mathlib.Order.Closure
ClosureOperator.closure_sup_closure_right : ∀ {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x y : α), c (x ⊔ c y) = c (x ⊔ y)
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j) {Z : C} (h : S.X₂.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS.δ i j hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.f j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Server.CodeActions.Basic
Lean.Server.CodeActionResolveData.mk.sizeOf_spec : ∀ (params : Lean.Lsp.CodeActionParams) (providerName : Lean.Name) (providerResultIndex : ℕ),
  sizeOf { params := params, providerName := providerName, providerResultIndex := providerResultIndex } =
    1 + sizeOf params + sizeOf providerName + sizeOf providerResultIndex
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.addY P Q = (-(Q 0 * P 2)) ^ 3 * P 1
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_congr_ae_trim : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) {P : MeasureTheory.Measure Ω} {X Y : Ω → ENNReal},
  X =ᵐ[P] Y → P⁻[X | mΩ] =ᵐ[P.trim hm] P⁻[Y | mΩ]
-- Init.Data.List.Lemmas
List.forall_mem_ne' : ∀ {α : Type u_1} {a : α} {l : List α}, (∀ a' ∈ l, ¬a' = a) ↔ a ∉ l
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.ε_η_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal] {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) h) =
    h
-- Mathlib.Order.CompleteLattice.Lemmas
biSup_inf_le_biSup_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (s : Set β) (a : α),
  ⨆ i ∈ s, f i ⊓ a ≤ (⨆ i ∈ s, f i) ⊓ a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.involutive_conjugate : ∀ (K : Type u_1) [inst : Field K], Function.Involutive NumberField.ComplexEmbedding.conjugate
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_left_self_sup : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R}, J * I ⊔ I = I
-- Lean.Data.Lsp.Internal
/-- Usage sites of the reference.  -/
Lean.Lsp.RefInfo.usages : Lean.Lsp.RefInfo → Array Lean.Lsp.RefInfo.Location
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.instBEqSign.beq_spec_1 : ∀ (x y : Float.Model.UnpackedFloat.Sign), (x == y) = (x.ctorIdx == y.ctorIdx)
-- Mathlib.Data.Finset.NAry
Finset.image₂_singleton_left' : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {t : Finset β} {a : α},
  Finset.image₂ f {a} t = Finset.image (f a) t
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- An absolutely monotone function on `s` is `C^∞` on `s`.  -/
AbsolutelyMonotoneOn.contDiffOn : ∀ {f : ℝ → ℝ} {s : Set ℝ}, AbsolutelyMonotoneOn f s → ContDiffOn ℝ (↑⊤) f s
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.symm_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  e.symm.symm = e
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.of_subsingleton_cod : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [Subsingleton α], HasProd f 1 L
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.weightIsModule : {R : Type u} → [inst : CommRing R] → (self : RootPairingCat R) → Module R self.weight
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCircuit_iff_minimal_not_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, C ⊆ M.E → (M.IsCircuit C ↔ Minimal (fun x => ¬M.Indep x) C)
-- Init.Data.Option.Lemmas
Option.any_filter : ∀ {α : Type u_1} {p q : α → Bool} (o : Option α), Option.any q (Option.filter p o) = Option.any (fun a => p a && q a) o
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftProp_subtype_val : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → ∀ (U : TopologicalSpace.Opens M), ChartedSpace.LiftProp Q Subtype.val
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.NonemptyParallelPairPresentationAux.hg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B)
  (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B),
  g =
    (CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ f g P₁ P₂).map
      { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ }
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.NonemptyParallelPairPresentationAux.ψ f g P₁ P₂)
        CategoryTheory.yoneda)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Hom.sum_sum_comp_sumAssoc : ∀ {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V}
  {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'}
  (f : G →g G') (g : H →g H') (h : I →g I'),
  (f.sum (g.sum h)).comp SimpleGraph.Iso.sumAssoc.toHom = SimpleGraph.Iso.sumAssoc.toHom.comp ((f.sum g).sum h)
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context.quotContext : Lean.MetavarContext.MkBindingM.Context → Lean.Name
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_sum' : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_8} (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M),
  Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, QuadraticMap.polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_bot : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R), I * ⊥ = ⊥
-- Init.Data.SInt.Lemmas
Int8.ofNat_toNatClampNeg : ∀ (x : Int8), 0 ≤ x → Int8.ofNat x.toNatClampNeg = x
-- Lean.Parser.Term
Lean.Parser.Term.letNegOpt : Lean.Parser.Parser
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.ext_iff : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {inst : LinearOrder ι} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  {inst_1 : SuccOrder ι} {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι}
  {x y : InverseSystem.PEquivOn f equivSucc s}, x = y ↔ x.equiv = y.equiv
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.one_le_blocks' : ∀ {n : ℕ} (c : Composition n) {i : ℕ} (h : i < c.length), 1 ≤ c.blocks[i]
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The upper part of the third column of the snake diagram is exact.  -/
CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  { X₁ := S.L₀.X₃, X₂ := S.L₁.X₃, X₃ := S.L₂.X₃, f := S.v₀₁.τ₃, g := S.v₁₂.τ₃, zero := ⋯ }.Exact
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The Gaussian pdf is strongly measurable.  -/
ProbabilityTheory.stronglyMeasurable_uncurry_gaussianPDFReal : MeasureTheory.StronglyMeasurable fun x =>
  match x with
  | (μ, v, x) => ProbabilityTheory.gaussianPDFReal μ v x
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_div : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), dist a b = ‖a / b‖
-- Mathlib.Data.Set.Restrict
Set.MapsTo.restrict_inj : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
  Function.Injective (Set.MapsTo.restrict f s t h) ↔ Set.InjOn f s
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.degreeOf_sub_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (i : σ) (p q : MvPolynomial σ R),
  MvPolynomial.degreeOf i (p - q) ≤ max (MvPolynomial.degreeOf i p) (MvPolynomial.degreeOf i q)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_prodMk' : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] (f : ι → M × N),
  Function.mulSupport f = (Function.mulSupport fun x => (f x).1) ∪ Function.mulSupport fun x => (f x).2
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- The multiplication of ordinals `a` and `b` is the order type of the lexicographic order on
`b × a`.  -/
Ordinal.monoid : Monoid Ordinal.{u}
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Conversion of normal form does not affect divisors.
 -/
MeromorphicOn.divisor_of_toMeromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → MeromorphicOn.divisor (toMeromorphicNFOn f U) U = MeromorphicOn.divisor f U
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.map_hom_inv'_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (F.map f.inv)) ((CategoryTheory.ConcreteCategory.hom (F.map f.hom)) x) = x
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2 =>
      h_3 size k v l size_2 k_2 v_2 l_1 r h r_2) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1
-- Std.Time.Date.Unit.Month
Std.Time.Month.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Month.Ordinal n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ofι_pt : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (ι : P ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g),
  (CategoryTheory.Limits.Fork.ofι ι w).pt = P
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.triangle : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ f₃ : α → E'},
  (fun x => f₁ x - f₂ x) =O[l] g → (fun x => f₂ x - f₃ x) =O[l] g → (fun x => f₁ x - f₃ x) =O[l] g
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  (∀ᵐ (a : α) ∂μ, f a ≤ g a) → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → {η : F ⟶ G} → Inhabited (CategoryTheory.Lax.OplaxTrans.Modification η η)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) X Y =
    CategoryTheory.MonObj.mul
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_coe : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ↑↑I = ↑I
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.card_pair_lcm_eq.f_surj : ∀ {n : ℕ},
  n ≠ 0 →
    ∀
      b ∈
        {x ∈ n.divisors ×ˢ n.divisors |
          match x with
          | (x, y) => x.lcm y = n},
      ∃ a, ∃ (ha : a ∈ Nat.finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f✝ a ha = b
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_comp_toList : ∀ {α : Type u_1}, ⇑FreeAddMonoid.ofList ∘ ⇑FreeAddMonoid.toList = id
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharThreeJNeZeroNF.a₃ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharThreeJNeZeroNF], W.a₃ = 0
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iio_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iio a)), Subtype.val '' Set.Iio b = Set.Iio ↑b
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.B.eq_1 : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) (K : Set F) (r s ε : ℝ),
  RightDerivMeasurableAux.B f K r s ε = ⋃ L ∈ K, RightDerivMeasurableAux.A f L r ε ∩ RightDerivMeasurableAux.A f L s ε
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_dual_eq_of_bijOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E : Set α},
  Set.BijOn f E N.E → (N.comapOn E f)✶ = N✶.comapOn E f
-- Mathlib.Data.Num.Bitwise
/-- A dependent induction principle for `NzsNum`, with base cases `0 : SNum` and `(-1) : SNum`.  -/
NzsNum.drec' : {C : SNum → Sort u_1} →
  ((b : Bool) → C (SNum.zero b)) → ((b : Bool) → (p : SNum) → C p → C (SNum.bit b p)) → (p : NzsNum) → C (SNum.nz p)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.intCast : ∀ {R : Type u_1} {f : ArithmeticFunction ℤ} [inst : Ring R], f.IsMultiplicative → (↑f).IsMultiplicative
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_cases : ∀ {x y : ℝ}, √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_mapRingEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R ≃+* S) (p : Polynomial R)
  (q : Polynomial S) (h : Associated (Polynomial.map (↑f) p) q),
  ⇑(AdjoinRoot.mapRingEquiv f p q h) = ⇑(AdjoinRoot.map (↑f) p q ⋯)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_min_max : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  Finset.Icc (min a b) (max a b) = Finset.uIcc a b
-- Mathlib.Data.Real.Basic
Real.instSemigroup : Semigroup ℝ
-- Mathlib.Analysis.Normed.Group.Basic
IndiscreteTopology.nnnorm_eq_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] [IndiscreteTopology E] (x : E), ‖x‖₊ = 0