mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.eq_def : ∀ (c : ℕ) (a : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.toPolyC.go c a =
    match a with
    | Lean.Grind.CommRing.Expr.num k => Lean.Grind.CommRing.Poly.num (k % ↑c)
    | Lean.Grind.CommRing.Expr.natCast k => Lean.Grind.CommRing.Poly.num (↑k % ↑c)
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num (k % ↑c)
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => (Lean.Grind.CommRing.Expr.toPolyC.go c a).combineC (Lean.Grind.CommRing.Expr.toPolyC.go c b) c
    | a.mul b => (Lean.Grind.CommRing.Expr.toPolyC.go c a).mulC (Lean.Grind.CommRing.Expr.toPolyC.go c b) c
    | a.neg => Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC.go c a) c
    | a.sub b =>
      (Lean.Grind.CommRing.Expr.toPolyC.go c a).combineC
        (Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC.go c b) c) c
    | a.pow k =>
      bif k == 0 then Lean.Grind.CommRing.Poly.num 1
      else
        match a with
        | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (n ^ k % ↑c)
        | Lean.Grind.CommRing.Expr.var x =>
          Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
        | x => (Lean.Grind.CommRing.Expr.toPolyC.go c a).powC k c
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.toRestrictTop_c : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  X.toRestrictTop.c = CategoryTheory.eqToHom ⋯
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.not : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
  FreeAddGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- Define the technical condition to be used as assumption in the inductive proof.  -/
Real.ContfracLegendre.Ass : ℝ → ℤ → ℤ → Prop
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_antitone_addSubmonoid : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α],
  Antitone fun P => AddAction.fixedPoints (↥P) α
-- Mathlib.Order.RelSeries
RelSeries.append_singleton_left : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r),
  (RelSeries.singleton r x).append p hx = p.cons x hx
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.cons : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  {rs : List R},
  IsSMulRegular M r →
    RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs → RingTheory.Sequence.IsWeaklyRegular M (r :: rs)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.ne_neg_self_iff : ∀ {θ : Real.Angle}, θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.equivProd_symm_apply_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (x : N × G),
  (SemidirectProduct.equivProd.symm x).right = x.2
-- Mathlib.LinearAlgebra.Dimension.Free
/-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`.  -/
Module.rank_lt_aleph0_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], Module.rank R M < Cardinal.aleph0 ↔ Module.Finite R M
-- Mathlib.Topology.Order.LawsonTopology
/-- `ofLawson` is the identity function from the `WithLawson` of a type.  -/
Topology.WithLawson.ofLawson : {α : Type u_1} → Topology.WithLawson α ≃ α
-- Mathlib.Topology.Order.MonotoneConvergence
/-- We say that `α` is a `SupConvergenceClass` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a least upper bound of `Set.range f`. Then `f x` tends to `𝓝 a`
as `x → ∞` (formally, at the filter `Filter.atTop`). We require this for `ι = (s : Set α)`,
`f = (↑)` in the definition, then prove it for any `f` in `tendsto_atTop_isLUB`.

This property holds for linear orders with order topology as well as their products.  -/
SupConvergenceClass : (α : Type u_3) → [Preorder α] → [TopologicalSpace α] → Prop
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_eq_algebraMap_mul_of : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : CommSemiring k] [inst_2 : MulSemiringAction G k]
  [inst_3 : SMulCommClass G k k] (a : G) (b : k),
  SkewMonoidAlgebra.single a b = (algebraMap k (SkewMonoidAlgebra k G)) b * (SkewMonoidAlgebra.of k G) a
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.Adhesive D] [CategoryTheory.Limits.HasPullbacks D]
  [CategoryTheory.Limits.HasPushouts D] [CategoryTheory.HasSheafify J D],
  CategoryTheory.Adhesive (CategoryTheory.Sheaf J D)
-- Mathlib.GroupTheory.Submonoid.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid.  -/
Submonoid.isMulCommutative_closure : ∀ (M : Type u_1) [inst : Monoid M] {s : Set M},
  (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → IsMulCommutative ↥(Submonoid.closure s)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Via the Yoneda lemma, `u : F.obj (op X)` defines a natural transformation `yoneda.obj X ⟶ F`
and via the element `η.app (op X) u` also a morphism `yoneda.obj X ⟶ A`. This structure
witnesses the fact that these morphisms form a commutative triangle with `η : F ⟶ A`, i.e.,
that `yoneda.obj X ⟶ F` lifts to a morphism in `Over A`.  -/
CategoryTheory.OverPresheafAux.MakesOverArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F ⟶ A) → {X : C} → (CategoryTheory.yoneda.obj X ⟶ A) → F.obj (Opposite.op X) → Prop
-- Mathlib.Algebra.GroupWithZero.Action.Opposite
/-- `Monoid.toOppositeMulAction` is faithful on nontrivial cancellative monoids with zero.  -/
IsLeftCancelMulZero.toFaithfulSMul_opposite : ∀ {α : Type u_2} [inst : MonoidWithZero α] [IsLeftCancelMulZero α], FaithfulSMul αᵐᵒᵖ α
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_inf : ∀ {M : Type u_2} [inst : AddZeroClass M] (S₁ S₂ : AddSubmonoid Mᵃᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Mathlib.Data.Real.Pointwise
Real.iSup_mul_of_nonneg : ∀ {ι : Sort u_1} {r : ℝ}, 0 ≤ r → ∀ (f : ι → ℝ), (⨆ i, f i) * r = ⨆ i, f i * r
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed.below.insertWff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2}
  {motive : (a : Lean.PrefixTreeNode α β cmp) → Lean.PrefixTreeNode.WellFormed cmp a → Prop}
  {t : Lean.PrefixTreeNode α β cmp} {k : List α} {val : β} (a : Lean.PrefixTreeNode.WellFormed cmp t),
  Lean.PrefixTreeNode.WellFormed.below a → motive t a → Lean.PrefixTreeNode.WellFormed.below ⋯
-- Std.Time.Format.Modifier
Std.Time.Modifier.S.injEq : ∀ (presentation presentation_1 : Std.Time.Fraction),
  (Std.Time.Modifier.S presentation = Std.Time.Modifier.S presentation_1) = (presentation = presentation_1)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with subtraction.  -/
ContDiffAt.laplacian_sub : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  ContDiffAt ℝ 2 f₁ x →
    ContDiffAt ℝ 2 f₂ x → Laplacian.laplacian (f₁ - f₂) x = Laplacian.laplacian f₁ x - Laplacian.laplacian f₂ x
-- Mathlib.CategoryTheory.Localization.Construction
/-- The isomorphism in `W.Localization` associated to a morphism `w` in W  -/
CategoryTheory.Localization.Construction.wIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (w : X ⟶ Y) → W w → (W.Q.obj X ≅ W.Q.obj Y)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.firstDart_mem_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil), p.firstDart hnil ∈ p.darts
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.insertIfNew k v t hl =
    if Std.DTreeMap.Internal.Impl.contains k t = true then
      { impl := t, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    else Std.DTreeMap.Internal.Impl.insert k v t ⋯
-- Mathlib.Topology.Category.LightProfinite.Basic
instEssSurjLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.EssSurj
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.iteratedDeriv_add_one_cosh : ∀ (n : ℕ), iteratedDeriv (n + 1) Complex.cosh = iteratedDeriv n Complex.sinh
-- Lean.Meta.Diagnostics
/-- Logs diagnostics and resets the counters  -/
Lean.Meta.reportDiag : Lean.MetaM Unit
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_right_le_size_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₂.size ≤ (t₁ ∪ t₂).size
-- Lean.Data.Lsp.Internal
Lean.Lsp.OpenNamespace.allExcept.inj : ∀ {«namespace» : Lean.Name} {exceptions : Array Lean.Name} {namespace_1 : Lean.Name} {exceptions_1 : Array Lean.Name},
  Lean.Lsp.OpenNamespace.allExcept «namespace» exceptions = Lean.Lsp.OpenNamespace.allExcept namespace_1 exceptions_1 →
    «namespace» = namespace_1 ∧ exceptions = exceptions_1
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_comp_of_left : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {H'' : Type u_8}
  [inst_11 : TopologicalSpace H''] {E'' : Type u_9} [inst_12 : NormedAddCommGroup E''] [inst_13 : NormedSpace 𝕜 E'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {g : M' → M''} {f : M → M'} {V : (x : M'') → TangentSpace I'' x} {s : Set M} {t : Set M'} {x₀ : M},
  MDiffAt[s] f x₀ →
    Set.MapsTo f s t →
      UniqueMDiffAt[s] x₀ →
        (mfderiv[t] g (f x₀)).IsInvertible →
          VectorField.mpullbackWithin I I'' (g ∘ f) V s x₀ =
            VectorField.mpullbackWithin I I' f (VectorField.mpullbackWithin I' I'' g V t) s x₀
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.nat.injEq : ∀ (n n_1 : ℕ), (Mathlib.Deriving.Encodable.S.nat✝ n = Mathlib.Deriving.Encodable.S.nat✝ n_1) = (n = n_1)
-- Std.Time.Date.Unit.Day
/-- Convert `Day.Offset` into `Second.Offset`.
 -/
Std.Time.Day.Offset.toSeconds : Std.Time.Day.Offset → Std.Time.Second.Offset
-- Init.Data.Order.MinMaxOn
maxOn_eq_if : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {a b : α},
  maxOn f a b = if f b ≤ f a then a else b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: The scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with `ℝ≥0`-valued functions.  -/
NNReal.inner_le_Lp_mul_Lq : ∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q : ℝ},
  p.HolderConjugate q → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.inter_isBasis_sInter : ∀ {α : Type u_2} {M : Matroid α} {I : Set α} {Xs : Set (Set α)},
  M.Indep I → Xs.Nonempty → (∀ X ∈ Xs, M.IsBasis (X ∩ I) X) → M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_iff_mul_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (a / b = c ↔ c * b = a)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The natural isomorphism `K.homology i ≅ (K.sc i).homology`
for all homological complexes `K`.  -/
HomologicalComplex.homologyFunctorIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          (i : ι) →
            [inst_2 : CategoryTheory.CategoryWithHomology C] →
              HomologicalComplex.homologyFunctor C c i ≅
                (HomologicalComplex.shortComplexFunctor C c i).comp (CategoryTheory.ShortComplex.homologyFunctor C)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_eq_headD_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.minD fallback = t.toList.headD fallback
-- Mathlib.Data.TypeVec
/-- right projection of a `prod` vector  -/
TypeVec.prod.snd : {n : ℕ} → {α β : TypeVec.{u} n} → (α.prod β).Arrow β
-- Mathlib.Topology.CompactOpen
/-- The uncurrying process is a continuous map between function spaces.  -/
ContinuousMap.continuous_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactSpace X] [inst_4 : LocallyCompactSpace Y],
  Continuous ContinuousMap.uncurry
-- Mathlib.GroupTheory.Coprod.Basic
/-- Map `AddMonoid.Coprod M N` to `AddMonoid.Coprod N M`
by applying `Sum.swap` to each element of the underlying list.

See also `AddEquiv.coprodComm` for an `AddEquiv` version.  -/
AddMonoid.Coprod.swap : (M : Type u_1) →
  (N : Type u_2) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → AddMonoid.Coprod M N →+ AddMonoid.Coprod N M
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is less than `WithZero.exp (-n)` if and only if
`r ∈ vⁿ`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R)
  (n : ℕ), v.intValuation r ≤ WithZero.exp (-↑n) ↔ r ∈ v.asIdeal ^ n
-- Mathlib.Topology.CompactOpen
Homeomorph.continuousMapOfUnique_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique X]
  (f : C(X, Y)), Homeomorph.continuousMapOfUnique.symm f = f default
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackLimitCone_isLimit : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit =
    (CategoryTheory.Limits.Types.pullbackCone f g).isLimitAux
      (fun s =>
        TypeCat.ofHom fun x =>
          ⟨((CategoryTheory.ConcreteCategory.hom s.fst) x, (CategoryTheory.ConcreteCategory.hom s.snd) x), ⋯⟩)
      ⋯ ⋯ ⋯
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Morphism of `C^n` monoids.  -/
ContMDiffMonoidMorphism : {𝕜 : 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] →
              {H' : Type u_5} →
                [inst_4 : TopologicalSpace H'] →
                  {E' : Type u_6} →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : NormedSpace 𝕜 E'] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E' H' →
                            WithTop ℕ∞ →
                              (G : Type u_8) →
                                [inst : TopologicalSpace G] →
                                  [ChartedSpace H G] →
                                    [Monoid G] →
                                      (G' : Type u_9) →
                                        [inst : TopologicalSpace G'] →
                                          [ChartedSpace H' G'] → [Monoid G'] → Type (max u_8 u_9)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.isometry : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), Isometry ⇑f
-- Mathlib.Order.BoundedOrder.Basic
bot_le : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderBot α] {a : α}, ⊥ ≤ a
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.mk : {α β σ : Type} →
  autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam →
    IO σ →
      (σ → α → Lean.ImportM β) →
        (β → α) →
          (σ → β → σ) →
            (σ → σ) → (Lean.Environment → α → Lean.OLeanEntries (Option α)) → Lean.ScopedEnvExtension.Descr α β σ
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The actual `NonUnitalStarSubalgebra` obtained from an element of a type satisfying
`NonUnitalSubsemiringClass`, `SMulMemClass` and `StarMemClass`.  -/
NonUnitalStarSubalgebra.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [inst_3 : Star A] →
              [inst_4 : SetLike S A] →
                [NonUnitalSubsemiringClass S A] →
                  [SMulMemClass S R A] → [StarMemClass S A] → S → NonUnitalStarSubalgebra R A
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.toFun_eq_coe : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S] (p : MulAlgebraNorm R S), p.toFun = ⇑p
-- Mathlib.Algebra.Homology.Homotopy
/-- The composition `f j (c.prev j) ≫ D.d (c.prev j) j`.  -/
prevD : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → (j : ι) → ((i j : ι) → C.X i ⟶ D.X j) →+ (C.X j ⟶ D.X j)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instInhabited : (K : Type u) → [inst : CommRing K] → Inhabited (RatFunc K)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries.0.Pentagonal.tendsto_order_neg_X_pow : ∀ (R : Type u_1) [inst : CommRing R] (k : ℕ),
  Filter.Tendsto (fun i => (-PowerSeries.X ^ (i + k + 1)).order) Filter.atTop (nhds ⊤)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.div_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {s : Set E}
  {x : E} {f : E → 𝕝}, AnalyticWithinAt 𝕜 f s x → ∀ {c : 𝕝}, AnalyticWithinAt 𝕜 (fun x => f x / c) s x
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.aedisjoint_compl_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.AEDisjoint μ s sᶜ
-- Mathlib.Data.List.Sym
List.Nodup.sym : ∀ {α : Type u_1} (n : ℕ) {xs : List α}, xs.Nodup → (List.sym n xs).Nodup
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.sub_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddGroup 𝕜] [inst_1 : LE α] (f g : IncidenceAlgebra 𝕜 α) (a b : α),
  (f - g) a b = f a b - g a b
-- Mathlib.Topology.Sets.Closeds
/-- See Note [custom simps projection].  -/
TopologicalSpace.Clopens.Simps.coe : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Clopens α → Set α
-- Init.PropLemmas
forall_or_imp_or_self_left_right : ∀ {α : Sort u_1} {P Q R : α → Prop}, (∀ (a : α), Q a ∨ P a → R a ∨ Q a) ↔ ∀ (a : α), P a → R a ∨ Q a
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.toUniqueSums : ∀ (G : Type u_1) [inst : Add G] [TwoUniqueSums G], UniqueSums G
-- Mathlib.LinearAlgebra.Determinant
/-- The determinants of a `LinearEquiv` and its inverse multiply to 1.  -/
LinearEquiv.det_mul_det_symm : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M ≃ₗ[A] M),
  LinearMap.det ↑f * LinearMap.det ↑f.symm = 1
-- Init.Internal.Order.Basic
Lean.Order.ImplicationOrder : Type
-- Mathlib.Order.Notation
Compl.mk : {α : Type u_1} → (α → α) → Compl α
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.mulIndicator_prod : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : CommMonoid β] (s : Finset ι) (t : Set κ) (f : ι → κ → β),
  t.mulIndicator (∏ i ∈ s, f i) = ∏ i ∈ s, t.mulIndicator (f i)
-- Mathlib.Algebra.Group.End
MulAut.coe_mul : ∀ (M : Type u_2) [inst : Mul M] (e₁ e₂ : MulAut M), ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.Cover.toPresieveOver.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] {X : CategoryTheory.Over S}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left)
  [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰],
  𝒰.toPresieveOver =
    CategoryTheory.Presieve.ofArrows (fun i => (𝒰.X i).asOver S) fun i => AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f i) S
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsClosedImmersion.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.hasLeftKanExtension : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) [w.GuitartExact]
  (F : CategoryTheory.Functor C₂ D) [R.HasPointwiseLeftKanExtension F], L.HasLeftKanExtension (T.comp F)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (toAlgEquiv : A ≃ₐ[R] B)
  (continuous_toFun : autoParam (Continuous toAlgEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toAlgEquiv.invFun) Homeomorph.continuous_invFun._autoParam)
  (toAlgEquiv_1 : A ≃ₐ[R] B)
  (continuous_toFun_1 : autoParam (Continuous toAlgEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun_1 : autoParam (Continuous toAlgEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam),
  ({ toAlgEquiv := toAlgEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAlgEquiv := toAlgEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toAlgEquiv = toAlgEquiv_1)
-- Mathlib.Data.ENat.Lattice
ENat.iSup_eq_zero : ∀ {ι : Sort u_1} {f : ι → ℕ∞}, iSup f = 0 ↔ ∀ (i : ι), f i = 0