mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.glue.eq_def : ∀ {α : Type u} {β : α → Type v} (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size),
  l.glue r hl hr hlr =
    match l, hl, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hl, hlr => r
    | Std.DTreeMap.Internal.Impl.inner sz k v l' r', hl, hlr =>
      match r, hr, hlr with
      | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => l
      | Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr =>
        if sz < sz' then
          match Std.DTreeMap.Internal.Impl.minView k' v' l'' r'' ⋯ ⋯ ⋯ with
          | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
            Std.DTreeMap.Internal.Impl.balanceLErase dk dv (Std.DTreeMap.Internal.Impl.inner sz k v l' r') dt hl ⋯ ⋯
        else
          match Std.DTreeMap.Internal.Impl.maxView k v l' r' ⋯ ⋯ ⋯ with
          | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
            Std.DTreeMap.Internal.Impl.balanceRErase dk dv dt (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') ⋯ hr
              ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- For any `s : S`, there is an `R`-linear map given by `a/b ↦ a/(b*s)`.
 -/
LocalizedModule.divBy : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      {M : Type v} →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → ↥S → LocalizedModule S M →ₗ[R] LocalizedModule S M
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- The bijection between the cells of `relativeCellComplex X` and the type
`X.N` of nondegenerate simplices of the simplicial set `X`.  -/
SSet.relativeCellComplexCellsEquiv : {X : SSet} → X.relativeCellComplex.Cells ≃ X.N
-- Mathlib.Combinatorics.Graph.Basic
Graph.Adj.left_mem : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β}, G.Adj x y → x ∈ G.vertexSet
-- Mathlib.Analysis.BoundedVariation
/-- Eta-expanded form of `eVariationOn_smul_le` -/
eVariationOn_fun_smul_le : ∀ {α : Type u_2} [inst : LinearOrder α] {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [inst_3 : NormedRing 𝕜] [inst_4 : NormedAlgebra ℝ 𝕜] [inst_5 : Module 𝕜 F]
  [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {C D : ENNReal} {s : Set α},
  (∀ x ∈ s, ‖f x‖ₑ ≤ C) →
    (∀ x ∈ s, ‖g x‖ₑ ≤ D) → eVariationOn (fun i => f i • g i) s ≤ C * eVariationOn g s + D * eVariationOn f s
-- Mathlib.Topology.Separation.Basic
/-- If a point in an R₁ space has a compact neighborhood,
then it has a basis of compact closed neighborhoods.  -/
IsCompact.isCompact_isClosed_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x : X} {L : Set X},
  IsCompact L → L ∈ nhds x → (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x
-- Mathlib.Topology.MetricSpace.Cauchy
/-- A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form `dist (u n) (u m) < B N` for all `n m ≥ N` are
converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast convergence to
`0`, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences.  -/
Metric.complete_of_convergent_controlled_sequences : ∀ {α : Type u} [inst : PseudoMetricSpace α] (B : ℕ → ℝ),
  (∀ (n : ℕ), 0 < B n) →
    (∀ (u : ℕ → α),
        (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) →
      CompleteSpace α
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The forgetful functor from the full subcategory of `Arrow T` defined by `P` to `Arrow T`.  -/
CategoryTheory.MorphismProperty.Arrow.forget : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q W : CategoryTheory.MorphismProperty T) →
      [inst_1 : Q.IsMultiplicative] →
        [inst_2 : W.IsMultiplicative] → CategoryTheory.Functor (P.Arrow Q W) (CategoryTheory.Arrow T)
-- Mathlib.Data.Part
Part.inter_def : ∀ {α : Type u_1} [inst : Inter α] (a b : Part α),
  a ∩ b = do
    let y ← a
    Part.map (fun x => y ∩ x) b
-- Mathlib.Algebra.Group.Equiv.Finite
Fintype.decidableEqAddEquivFintype : {α : Type u_4} →
  {β : Type u_5} → [DecidableEq β] → [Fintype α] → [inst : Add α] → [inst_1 : Add β] → DecidableEq (α ≃+ β)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_lift_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α σ : Type u}
  {post : α → σ → Pred} {epost : EPred} (x : m α),
  Std.Internal.Do.wp (StateT.lift x) post epost = Std.Internal.Do.wp (MonadLift.monadLift x) post epost
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_erase : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
  (Polynomial.erase n p).toFinsupp = AddMonoidAlgebra.erase n p.toFinsupp
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxInv.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S], IsLocalization.Away.auxInv✝ S r = IsLocalization.Away.lift r ⋯
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler : Type
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_inv_eq_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] (s : Finset α), Finset.image (fun x => x⁻¹) s = s⁻¹
-- Mathlib.Algebra.Group.Shrink
equivShrink_mul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α] (x y : α),
  (equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y
-- Mathlib.Tactic.Widget.SelectPanelUtils
SelectInsertParams.mk.injEq : ∀ (pos : Lean.Lsp.Position) (goals : Array Lean.Widget.InteractiveGoal)
  (selectedLocations : Array Lean.SubExpr.GoalsLocation) (replaceRange : Lean.Lsp.Range) (pos_1 : Lean.Lsp.Position)
  (goals_1 : Array Lean.Widget.InteractiveGoal) (selectedLocations_1 : Array Lean.SubExpr.GoalsLocation)
  (replaceRange_1 : Lean.Lsp.Range),
  ({ pos := pos, goals := goals, selectedLocations := selectedLocations, replaceRange := replaceRange } =
      { pos := pos_1, goals := goals_1, selectedLocations := selectedLocations_1, replaceRange := replaceRange_1 }) =
    (pos = pos_1 ∧ goals = goals_1 ∧ selectedLocations = selectedLocations_1 ∧ replaceRange = replaceRange_1)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_le_iff_dist_coe_center_le : ∀ {z w : UpperHalfPlane} {r : ℝ}, dist z w ≤ r ↔ dist ↑z ↑(w.center r) ≤ w.im * Real.sinh r
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_domain_sSup_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {c : Set (E →ₛₗ.[σ] F)},
  c.Nonempty →
    ∀ (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c) {x : E}, x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain
-- Mathlib.Order.Hom.BoundedLattice
instCoeTCBoundedLatticeHomOfBoundedLatticeHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Lattice α] →
          [inst_2 : Lattice β] →
            [inst_3 : BoundedOrder α] →
              [inst_4 : BoundedOrder β] → [BoundedLatticeHomClass F α β] → CoeTC F (BoundedLatticeHom α β)
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.pos : ∀ {p : ℕ}, Nat.Prime p → 0 < p
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.integral_condKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℝ E] (a : α),
  MeasureTheory.Integrable f (κ a) →
    ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂κ a
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const_map_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {X Y : C} (f : X ⟶ Y) (x : J), ((CategoryTheory.Functor.const J).map f).app x = f
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ofHom_comp : ∀ {X Y Z : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] [inst_2 : Semigroup Z] (f : X →ₙ* Y) (g : Y →ₙ* Z),
  Semigrp.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (Semigrp.ofHom f) (Semigrp.ofHom g)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The power series that is equal to
$\frac{1}{2πi}\sum_{n=0}^{\infty}
  \oint_{|z-c|=R} \left(\frac{w-c}{z - c}\right)^n \frac{1}{z-c}f(z)\,dz$ at
`w - c`. The coefficients of this power series depend only on `f ∘ circleMap c R`, and the power
series converges to `f w` if `f` is differentiable on the closed ball `Metric.closedBall c R` and
`w` belongs to the corresponding open ball. For any circle integrable function `f`, this power
series converges to the Cauchy integral for `f`.  -/
cauchyPowerSeries : {E : Type u_1} →
  [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → (ℂ → E) → ℂ → ℝ → FormalMultilinearSeries ℂ ℂ E
-- Lean.Elab.Term.TermElabM
/-- Pushes the transformation inwards by one level, allowing transformation-correct access to fields.
 -/
Lean.Elab.Tactic.TacticParsedSnapshot.applyTransform : Lean.Elab.Tactic.TacticParsedSnapshot → Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.mk_coe : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B) (e' : B → A)
  (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₅ :
    ∀ (a : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) =
        star ({ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a))
  (h₆ :
    ∀ (r : R) (a : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
              map_star' := h₅ }.toFun
          (r • a) =
        r •
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
                map_star' := h₅ }.toFun
            a),
  { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅,
      map_smul' := h₆ } =
    e
-- Mathlib.Tactic.Order.Graph.Tarjan
Mathlib.Tactic.Order.Graph.TarjanState.mk : Mathlib.Tactic.Order.Graph.DFSState →
  Std.HashMap ℕ ℕ → Std.HashMap ℕ ℕ → Array ℕ → Std.HashSet ℕ → ℕ → Mathlib.Tactic.Order.Graph.TarjanState
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_of_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (FreeMonoid.lift fun x => FreeMonoid.of (f x)) = FreeMonoid.map f
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fst_comp_inr : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  (OrderMonoidHom.fst α β).comp (OrderMonoidHom.inr α β) = 1
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.dualEquiv_inverse : FinBddDistLat.dualEquiv.inverse = FinBddDistLat.dual
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The continuous linear map from a C⋆-algebra `A` to the `PositiveLinearMap.preGNS` space induced by
a positive linear functional `f : A →ₚ[ℂ] ℂ`. This map is given by left-multiplication by `a`:
`x ↦ f.toPreGNS (a * f.ofPreGNS x)`.

This is the map that is lifted to the completion of `f.PreGNS` (i.e. `f.GNS`) in order to define
`gnsNonUnitalStarAlgHom`.
 -/
PositiveLinearMap.leftMulMapPreGNS : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → [inst_2 : StarOrderedRing A] → A → f.PreGNS →L[ℂ] f.PreGNS
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.instMonadCommRingM : Lean.Meta.Grind.Arith.CommRing.MonadCommRing Lean.Meta.Grind.Arith.CommRing.M✝
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.regular.inj : ∀ {b b_1 : Aesop.BuilderName}, Aesop.Frontend.DBuilderName.regular b = Aesop.Frontend.DBuilderName.regular b_1 → b = b_1
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- If `Y Y'` have an exact pairing,
then the functor `tensor_right Y` is left adjoint to `tensor_right Y'`.
 -/
CategoryTheory.tensorRightAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (Y Y' : C) →
        [CategoryTheory.ExactPairing Y Y'] →
          CategoryTheory.MonoidalCategory.tensorRight Y ⊣ CategoryTheory.MonoidalCategory.tensorRight Y'
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.toCentralizer_equivariant : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (c : ↥g.cycleFactorsFinset) (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)), a.toCentralizer τ • c = ↑τ c
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) (x : ↑((M.restrict f).presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom)
      ((CategoryTheory.ConcreteCategory.hom ((M.restrict f).presheaf.map hUV)) x) =
    (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE ⋯).op))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).hom) x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Version of `TStructure.triangle_map_ext` that is specialized for the auxiliary
definition `TruncAux.triangle`.  -/
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_map_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C}
  (f₁ f₂ :
    CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X ⟶
      CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n Y),
  autoParam (f₁.hom₂ = f₂.hom₂) CategoryTheory.Triangulated.TStructure.TruncAux.triangle_map_ext'._auto_1✝ → f₁ = f₂
-- Init.Data.Nat.Lemmas
Nat.shiftLeft_add : ∀ (m n k : ℕ), m <<< (n + k) = m <<< n <<< k
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.seminormedGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)],
  Pi.seminormedGroup =
    { norm := fun f => ↑(Finset.univ.sup fun b => ‖f b‖₊), toGroup := Pi.group,
      toPseudoMetricSpace := pseudoMetricSpacePi, dist_eq := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_smul : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] (M : Matrix n n R)
  (c : R), (c • M).permanent = c ^ Fintype.card n * M.permanent
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.germ_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx) (AlgebraicGeometry.Scheme.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)
-- Mathlib.LinearAlgebra.Dual.Defs
Module.Dual.eval_naturality : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂),
  f.dualMap.dualMap ∘ₗ Module.Dual.eval R M₁ = Module.Dual.eval R M₂ ∘ₗ f
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
CommCStarAlgebra.nnnorm_add_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCommCStarAlgebra A] {a b : A}, a * b = 0 → ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The function from `Spec A⁰_f` to `Proj|D(f)` is defined by `q ↦ {a | aᵢᵐ/fⁱ ∈ q}`, i.e. sending
`q` a prime ideal in `A⁰_f` to the homogeneous prime relevant ideal containing only and all the
elements `a : A` such that for every `i`, the degree 0 element formed by dividing the `m`-th power
of the `i`-th projection of `a` by the `i`-th power of the degree-`m` homogeneous element `f`,
lies in `q`.

The set `{a | aᵢᵐ/fⁱ ∈ q}`
* is an ideal, as proved in `carrier.asIdeal`;
* is homogeneous, as proved in `carrier.asHomogeneousIdeal`;
* is prime, as proved in `carrier.asIdeal.prime`;
* is relevant, as proved in `carrier.relevant`.
 -/
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                              (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace →
                      Set A
-- Mathlib.Topology.Instances.Real.Lemmas
/-- The limit of an antitone, bounded below sequence `f : ℕ → ℝ` on `Ici k` is a greatest
lower bound of the sequence.  -/
Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici : ∀ {f : ℕ → ℝ} {k : ℕ} {x : ℝ},
  Filter.Tendsto f Filter.atTop (nhds x) →
    AntitoneOn f (Set.Ici k) → BddBelow (f '' Set.Ici k) → IsGLB (f '' Set.Ici k) x
-- Mathlib.Analysis.InnerProductSpace.Trace
LinearMap.IsSymmetric.re_trace_eq_sum_eigenvalues : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric),
  RCLike.re ((LinearMap.trace 𝕜 E) T) = ∑ i, hT.eigenvalues hn i
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.eq_inf : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T},
  CompleteLattice.MulticoequalizerDiagram x u v → ∀ (i j : ι), v i j = u i ⊓ u j
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) {Z : V} (h : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₃₂).inv h) =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h
-- Mathlib.Order.Defs.Unbundled
IsLinearOrder.toTotal : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsLinearOrder α r], Std.Total r
-- Mathlib.Algebra.Order.Floor.Defs
instFloorSemiringNat : FloorSemiring ℕ
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.id_nondegenerate : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], LinearMap.id.Nondegenerate
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.eq_1 : ∀ {α : Type u}, FreeAddGroup.Red = Relation.ReflTransGen FreeAddGroup.Red.Step
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_comm : ∀ {R : Type u_9} {M : Type u_10} {I : Type u_11} {J : Type u_12} [inst : PartialOrder R] [inst_1 : CommSemiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R I)
  (g : Convexity.StdSimplex R J) (e : I → J → M),
  (Convexity.iConvexComb f fun i => Convexity.iConvexComb g (e i)) =
    Convexity.iConvexComb g fun j => Convexity.iConvexComb f fun i => e i j
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_zero : ∀ {R : Type u} [inst : Semiring R], { toFinsupp := 0 } = 0
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C}
  {πX : X ⟶ S} (i : I) (t t_1 : A i ⟶ X) (e_t : t = t_1) (b b_1 : B i ⟶ S) (e_b : b = b_1)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b),
  { i := i, t := t, b := b, w := w } = { i := i, t := t_1, b := b_1, w := ⋯ }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mul_const : ∀ {A : Type u_7} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → A},
  IntervalIntegrable f μ a b → ∀ (c : A), IntervalIntegrable (fun x => f x * c) μ a b
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.HasPullbacks.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Presieve X} {Y : C} {f : Y ⟶ X},
  (∀ {Z : C} {h : Z ⟶ X}, R h → CategoryTheory.Limits.HasPullback h f) → R.HasPullbacks f
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.trans : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B C : Set E}, IsExtreme 𝕜 A B → IsExtreme 𝕜 B C → IsExtreme 𝕜 A C
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.forIn'_eq_match.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (next : α) (h_1 : some next = none → motive none)
  (h_2 : (next_1 : α) → some next = some next_1 → motive (some next_1)),
  (match hs : some next with
    | none => h_1 hs
    | some next_1 => h_2 next_1 hs) =
    h_2 next ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.mappingCone_triangle_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle φ) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Batteries.Data.Array.Pairwise
Array.pairwise_append : ∀ {α : Type u_1} {R : α → α → Prop} {as bs : Array α},
  Array.Pairwise R (as ++ bs) ↔ Array.Pairwise R as ∧ Array.Pairwise R bs ∧ ∀ x ∈ as, ∀ y ∈ bs, R x y
-- Init.Data.UInt.Lemmas
UInt8.ofFin_sub : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a - b) = UInt8.ofFin a - UInt8.ofFin b
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isLUB_inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G},
  IsLUB s⁻¹ a ↔ IsGLB s a⁻¹