mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAdd.of_le : ∀ {𝕜 : 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 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {m n : WithTop ℕ∞},
  m ≤ n → ∀ [h : ContMDiffAdd I n G], ContMDiffAdd I m G
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.commShiftIso_inv_naturality : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] {X Y : C}
  (f : X ⟶ Y) (a : A),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f))
      ((CategoryTheory.Functor.commShiftIso F a).inv.app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
      (F.map ((CategoryTheory.shiftFunctor C a).map f))
-- Mathlib.Algebra.Regular.Basic
IsAddRightRegular.add_right_eq_self_iff : ∀ {R : Type u_1} [inst : AddMonoid R] {a b : R}, IsAddRightRegular a → (b + a = a ↔ b = 0)
-- Mathlib.Order.RelIso.Basic
Equiv.emptySum.congr_simp : ∀ (α : Type u_9) (β : Type u_10) [inst : IsEmpty α], Equiv.emptySum α β = Equiv.emptySum α β
-- Mathlib.NumberTheory.SmoothNumbers
/-- The `Finset` of prime factors of an `n`-smooth number is contained in the `Finset`
of primes below `n`.  -/
Nat.primeFactors_subset_of_mem_smoothNumbers : ∀ {m n : ℕ}, m ∈ n.smoothNumbers → m.primeFactors ⊆ n.primesBelow
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- Constructor for `FibrantObject C`.  -/
HomotopicalAlgebra.FibrantObject.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] →
      [inst_2 : CategoryTheory.Limits.HasTerminal C] →
        (X : C) → [HomotopicalAlgebra.IsFibrant X] → HomotopicalAlgebra.FibrantObject C
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.foldM_eq_foldlM_toList : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.DHashMap.Raw.foldM f init ↑m = List.foldlM (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toList ↑m)
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.coe_cons : ∀ {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ Set.range ⇑x), ⇑(Fin.Embedding.cons x ha) = Fin.cons a ⇑x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_assoc' : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z))
        (CategoryTheory.eComp V W X Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z))
      (CategoryTheory.eComp V W Y Z)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} [inst_1 : Inhabited (β k)],
  (m₁.union m₂ ⋯ ⋯).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.ext : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] (rels : FreeMonoid α → FreeMonoid α → Prop)
  {φ ψ : PresentedMonoid rels →* M}, (∀ (x : α), φ (PresentedMonoid.of rels x) = ψ (PresentedMonoid.of rels x)) → φ = ψ
-- Mathlib.Order.SuccPred.Basic
Order.Iic_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] (a : α),
  Set.Iic (Order.succ a) = insert (Order.succ a) (Set.Iic a)
-- Mathlib.Order.OrderDual
OrderDual.Ord.dual_dual : ∀ (α : Type u_2) [H : Ord α], OrderDual.instOrd αᵒᵈ = H
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.conditionallyCompleteLattice.eq_1 : ∀ {α : Type u_5} [inst : ConditionallyCompleteLattice α],
  WithBot.conditionallyCompleteLattice =
    { toLattice := WithBot.lattice, toSupSet := WithBot.instSupSet, toInfSet := WithBot.instInfSet, isLUB_csSup := ⋯,
      isGLB_csInf := ⋯ }
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_cons_succ : ∀ {α : Type u_1} {a : α} {i : ℕ} {l : List α}, (a :: l)[i + 1]? = l[i]?
-- Mathlib.Lean.Expr.Basic
/-- `aux depth e n` checks whether the body of the `n`-th lambda of `e` has loose bvar
`depth - 1`.  -/
_private.Mathlib.Lean.Expr.Basic.0.Lean.Expr.isConstantApplication.aux : ℕ → Lean.Expr → ℕ → Bool
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.eq_of_comp_right_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : Y ⟶ X},
  (∀ {Z : C} (h : Z ⟶ Y), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimitRecOn_of_isPredPrelimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  (pred : (a : α) → ¬IsMin a → motive (Order.pred a)) (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → motive a)
  (hb : Order.IsPredPrelimit b), Order.isPredPrelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb
-- Init.Data.String.Lemmas.Pattern.Split.Char
_private.Init.Data.String.Lemmas.Pattern.Split.Char.0.String.Slice.Pattern.Model.split.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (pos : s.Pos) → none = some pos → motive (some pos))
  (h_2 : none = none → motive none),
  (match hd : none with
    | some pos => h_1 pos hd
    | none => h_2 hd) =
    h_2 ⋯
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              (F : CategoryTheory.Functor A B) →
                [inst_3 : CategoryTheory.HasWeakSheafify J B] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                    [J.PreservesSheafification F] →
                      CategoryTheory.Localization.Lifting (CategoryTheory.presheafToSheaf J A) J.W
                        (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp
                          (CategoryTheory.presheafToSheaf J B))
                        (CategoryTheory.Sheaf.composeAndSheafify J F)
-- Mathlib.Analysis.Convex.Birkhoff
/-- If M is a doubly stochastic matrix, then it is a convex combination of permutation matrices. Note
`doublyStochastic_eq_convexHull_permMatrix` shows `doublyStochastic n` is exactly the convex hull of
the permutation matrices, and this lemma is instead most useful for accessing the coefficients of
each permutation matrices directly.
 -/
exists_eq_sum_perm_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Field R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n →
    ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.isBoxedName : Lean.Name → Bool
-- Mathlib.RingTheory.Spectrum.Prime.LTSeries
PrimeSpectrum.exist_mem_one_of_mem_maximal_ideal : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {p₁ p₀ : PrimeSpectrum R},
  p₀ < p₁ →
    p₁ < IsLocalRing.closedPoint R →
      ∀ {x : R}, x ∈ IsLocalRing.maximalIdeal R → ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < IsLocalRing.maximalIdeal R
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.mk.sizeOf_spec : ∀ (map : Lean.MVarIdMap Lean.MVarId), sizeOf { map := map } = 1 + sizeOf map
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Bitwise and.
 -/
Std.Tactic.BVDecide.BVBinOp.and : Std.Tactic.BVDecide.BVBinOp
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
/-- If `U ∌ 0` is an open set on the real line and `V` is an open set on a sphere of nonzero radius,
then their pointwise scalar product is an open set.  -/
IsOpen.smul_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  r ≠ 0 → ∀ {U : Set ℝ} {V : Set ↑(Metric.sphere 0 r)}, IsOpen U → 0 ∉ U → IsOpen V → IsOpen (U • Subtype.val '' V)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.notMem_sInter_of_notMem : ∀ {x y z : ZFSet.{u_1}}, y ∉ z → z ∈ x → y ∉ x.sInter
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C}
  (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂) ⟶ A)
  (h :
    CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0)
  (hn₁ : n₀ + 1 = n₁) (h' : CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE._auto_1),
  CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁)
      (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
        (X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂)) =
    x
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.lift_toCoprod_inl_eq_inl_mk : ∀ {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)),
  (FreeGroup.lift (PresentedGroup.toCoprod rels₁ rels₂)).comp (FreeGroup.map Sum.inl) =
    Monoid.Coprod.inl.comp (PresentedGroup.mk rels₁)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.empty_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (t : Finset β), ∅ • t = ∅
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abLeftHomologyData_f' : ∀ (S : CategoryTheory.ShortComplex Ab), S.abLeftHomologyData.f' = AddCommGrpCat.ofHom S.abToCycles
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeFunctor_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G), (e.changeFunctor iso).functor = G
-- Mathlib.RingTheory.HahnSeries.Summable
/-- The infinite sum of a `SummableFamily` of Hahn series.  -/
HahnSeries.SummableFamily.hsum : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → HahnSeries.SummableFamily Γ R α → HahnSeries Γ R
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.image_of_isOpenMap_of_isOpen : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsDiscrete s → IsOpenMap f → IsOpen s → IsDiscrete (f '' s)
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.squashSeq.match_1.eq_2 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) × Option (GenContFract.Pair K) → Sort u_2)
  (x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K))
  (h_1 : (gp_n gp_succ_n : GenContFract.Pair K) → motive (some gp_n, some gp_succ_n))
  (h_2 : (x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K)) → motive x),
  (∀ (gp_n gp_succ_n : GenContFract.Pair K), x = (some gp_n, some gp_succ_n) → False) →
    (match x with
      | (some gp_n, some gp_succ_n) => h_1 gp_n gp_succ_n
      | x => h_2 x) =
      h_2 x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulActionHomClass F M X Y` states that `F` is a type of
morphisms which are equivariant with respect to actions of `M`
This is an abbreviation of `MulActionSemiHomClass`.  -/
AddActionHomClass : (F : Type u_8) →
  (M : outParam (Type u_9)) →
    (X : outParam (Type u_10)) → (Y : outParam (Type u_11)) → [VAdd M X] → [VAdd M Y] → [FunLike F X Y] → Prop
-- Mathlib.Topology.MetricSpace.HausdorffDimension
ContinuousLinearEquiv.dimH_univ : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E ≃L[𝕜] F),
  dimH Set.univ = dimH Set.univ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.dim_p : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] (x : ↑P.II), (↑(P.p x)).dim = (↑x).dim + 1
-- Mathlib.Order.IsNormal
Order.IsNormal.apply_of_isSuccLimit : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [inst : ConditionallyCompleteLinearOrderBot α]
  [inst_1 : ConditionallyCompleteLinearOrder β], Order.IsNormal f → Order.IsSuccLimit a → f a = ⨆ b, f ↑b
-- Mathlib.Algebra.GradedMonoid
SetLike.GradeZero.coe_mul : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [inst_3 : SetLike.GradedMonoid A] (a b : ↥(A 0)), ↑(a * b) = ↑a * ↑b
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.isLUB_of_u_image : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β] (gi : GaloisInsertion l u)
  {s : Set β} {a : α}, IsLUB (u '' s) a → IsLUB s (l a)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.curry_zero : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), F.curry 0 = f₀
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.zero_vlt_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, 0 <ᵥ x → 0 <ᵥ y → 0 <ᵥ x * y
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.sub_iff_right` -/
DifferentiableOn.fun_sub_iff_right : ∀ {𝕜 : 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] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → (DifferentiableOn 𝕜 (fun i => f i - g i) s ↔ DifferentiableOn 𝕜 g s)
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is a commutative group.  -/
Subgroup.closureCommGroupOfComm : {G : Type u_1} → [inst : Group G] → {k : Set G} → (∀ x ∈ k, ∀ y ∈ k, x * y = y * x) → CommGroup ↥(Subgroup.closure k)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- Homeomorphism between `X² = Fin 2 → X` and `X × X`.  -/
Homeomorph.finTwoArrow : {X : Type u_1} → [inst : TopologicalSpace X] → (Fin 2 → X) ≃ₜ X × X
-- Mathlib.Analysis.Distribution.TemperedDistribution
Function.HasTemperateGrowth.toTemperedDistribution_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : SecondCountableTopology E]
  (μ : autoParam (MeasureTheory.Measure E) _auto_44✝) [hμ : μ.HasTemperateGrowth] {f : E → F}
  (hf : Function.HasTemperateGrowth f) (g : SchwartzMap E ℂ),
  (Function.HasTemperateGrowth.toTemperedDistribution μ hf) g = ∫ (x : E), g x • f x ∂μ
-- Init.Prelude
/-- Gets the current namespace given the position in the file.  -/
Lean.Macro.getCurrNamespace : Lean.MacroM Lean.Name
-- Mathlib.Order.Category.Frm
Frm.hom_ext : ∀ {X Y : Frm} {f g : X ⟶ Y}, Frm.Hom.hom f = Frm.Hom.hom g → f = g
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Mapping from variables to their denotations.
Remark each variable can be in only one ring.
 -/
Lean.Meta.Grind.AC.Struct.vars : Lean.Meta.Grind.AC.Struct → Lean.PArray Lean.Expr
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b) (r : R), (v.adicAbv hb) ((algebraMap R K) r) ≤ 1
-- Mathlib.Tactic.Polynomial.Basic
/-- `polynomial` solves equalities of `Polynomial`s and similar types.

Given a goal which is an equality in `Polynomial R` with a commutative ring `R`, `polynomial`
turns both sides of the equation into a normal form by expanding out the brackets. It then closes
the goal if both sides contain the same terms and fails otherwise. `polynomial_nf` normalizes all
subexpressions at a given location.

Variants of `polynomial` include:
* `polynomial`: normalize both sides of an equation and close the goal if they are equal
* `polynomial!`: run `polynomial` at default transparency
* `polynomial_nf`: normalize all subexpression of the goal
* `polynomial_nf at h₁ h₂ ⊢`: normalize all subexpressions at hypotheses `h₁` `h₁` and the goal
* `polynomial_nf at *`: normalize all subexpressions of all local hypotheses and the goal
* `polynomial_nf!`: run `polynomial_nf` at default transparency

The `polynomial` tactic can be extended to work with algebras other than `Polynomial` using the
attributes `polynomial_infer_base`, `polynomial_pre` and `polynomial_post`. This is only possible
if the base ring can be inferred from the structure of the type.

Examples:

```
example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h
```

 -/
Mathlib.Tactic.Polynomial.tacticPolynomial_nf!_ : Lean.ParserDescr
-- Mathlib.Data.DFinsupp.Order
DFinsupp.le_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : DecidableEq ι] [inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)]
  {f g : Π₀ (i : ι), α i}, f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.zero_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (x : A), 0 x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.fork_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  (CategoryTheory.Limits.equalizer.fork f g).ι = CategoryTheory.Limits.equalizer.ι f g
-- Mathlib.Analysis.Convex.Quasiconvex
QuasilinearOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasilinearOn 𝕜 s f → QuasilinearOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Lean.Elab.DeprecatedArg
Lean.Elab.deprecatedArgExt : Lean.SimplePersistentEnvExtension Lean.Elab.DeprecatedArgEntry Lean.Elab.DeprecatedArgState
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_totalDegree_le : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] (M : Matrix m n R) (i : m),
  (M.toMvPolynomial i).totalDegree ≤ 1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The star algebra equivalence between the linear endomorphisms of finite-dimensional inner
product space and square matrices induced by the choice of an orthonormal basis.  -/
LinearMap.toMatrixOrthonormal : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {n : Type u_6} →
            [inst_3 : Fintype n] →
              [DecidableEq n] →
                [inst_5 : FiniteDimensional 𝕜 E] → OrthonormalBasis n 𝕜 E → (E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜
-- Std.Async.Basic
Std.Async.MaybeTask.pure : {α : Type} → α → Std.Async.MaybeTask α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
CochainComplex.HomComplex.Cochain.InductionUp.sequence_eqUpTo : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {d : ℤ} {X : ℕ → Set (CochainComplex.HomComplex.Cochain K L d)}
  (φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))) {p₀ : ℤ},
  (∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)) →
    ∀ (x₀ : ↑(X 0)) (n₁ n₂ : ℕ),
      n₁ ≤ n₂ →
        (↑(CochainComplex.HomComplex.Cochain.InductionUp.sequence φ x₀ n₁)).EqUpTo
          (↑(CochainComplex.HomComplex.Cochain.InductionUp.sequence φ x₀ n₂)) (p₀ + ↑n₁)
-- Mathlib.Probability.Martingale.Convergence
/-- **Almost everywhere martingale convergence theorem**: An L¹-bounded submartingale converges
almost everywhere to a `⨆ n, ℱ n`-measurable function.  -/
MeasureTheory.Submartingale.ae_tendsto_limitProcess : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess f ℱ μ ω))
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.isTopologicalRing : ∀ (self : TopCommRingCat), IsTopologicalRing self.α
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T₁ T₂ : CategoryTheory.Monad C}
  {x y : CategoryTheory.MonadHom T₁ T₂}, x = y ↔ x.app = y.app
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A simple graph `G` is inducingly contained in a simple graph `H` if there exists an induced
subgraph of `H` isomorphic to `G`. This is denoted by `G ⊴ H`.  -/
SimpleGraph.«term_⊴_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- The main objects in this lemma fit in the following commutative diagram:
```
Pfg -------> X <------- Pfi
 |           |           |
 |           f           |
 ↓           ↓           ↓
 Y --- g --> S <-- i --- Z
  \                     /
    --              --
       \          /
         --  R --
```
Suppose the two squares are cartesian, then `Pfg ×[Y] R` is the pullback of
`Pfi ⟶ Z` and `R ⟶ Z`.
 -/
CategoryTheory.IsPullback.paste_twist_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z S : C} {f : X ⟶ S} {g : Y ⟶ S} {i : Z ⟶ S} {Pfg : C}
  {fstfg : Pfg ⟶ X} {sndfg : Pfg ⟶ Y},
  CategoryTheory.IsPullback fstfg sndfg f g →
    ∀ {Pfi : C} {fstfi : Pfi ⟶ X} {sndfi : Pfi ⟶ Z},
      CategoryTheory.IsPullback fstfi sndfi f i →
        ∀ {R : C} (rY : R ⟶ Y) (rZ : R ⟶ Z),
          CategoryTheory.CategoryStruct.comp rY g = CategoryTheory.CategoryStruct.comp rZ i →
            ∀ {Psndfgr : C} (fstsndfgr : Psndfgr ⟶ Pfg) (sndsndfgr : Psndfgr ⟶ R),
              CategoryTheory.IsPullback fstsndfgr sndsndfgr sndfg rY →
                ∀ {t : Psndfgr ⟶ Pfi},
                  CategoryTheory.CategoryStruct.comp t fstfi = CategoryTheory.CategoryStruct.comp fstsndfgr fstfg →
                    CategoryTheory.CategoryStruct.comp t sndfi = CategoryTheory.CategoryStruct.comp sndsndfgr rZ →
                      CategoryTheory.IsPullback t sndsndfgr sndfi rZ