mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_eq : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.C R n = Polynomial.X * Polynomial.Chebyshev.C R (n - 1) - Polynomial.Chebyshev.C R (n - 2)
-- Mathlib.Algebra.Algebra.Hom.Rat
RingHom.toRatAlgHom_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R →+* S) (x : R), f.toRatAlgHom x = f x
-- Init.Data.String.Basic
String.Internal.toArray.eq_1 : ∀ (b : String), String.Internal.toArray b = b.toByteArray.utf8Decode?.get ⋯
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (e e_1 : (i : ι) → D₁.obj i ≅ D₂.obj i) (e_e : e = e_1)
  (comm :
    ∀ (i₁ i₂ : ι),
      CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) =
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom)),
  CategoryTheory.Pseudofunctor.DescentData'.isoMk e comm = CategoryTheory.Pseudofunctor.DescentData'.isoMk e_1 ⋯
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.coe_symmMeasurableEquiv : ⇑unitInterval.symmMeasurableEquiv = unitInterval.symm
-- Mathlib.Algebra.Group.Center
Set.centralizer_univ : ∀ (M : Type u_1) [inst : Semigroup M], Set.univ.centralizer = Set.center M
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types.
 -/
_private.Lean.PrettyPrinter.Delaborator.FieldNotation.0.Lean.PrettyPrinter.Delaborator.typeMatchesBaseName : Lean.Expr → Lean.Name → Lean.MetaM Bool
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_finset_sup' : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ),
  (s.sup' H p).closedBall e r = s.inf' H fun i => (p i).closedBall e r
-- Mathlib.Analysis.Calculus.Deriv.Basic
toSpanSingleton_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, ContinuousLinearMap.toSpanSingleton 𝕜 (deriv f x) = fderiv 𝕜 f x
-- Init.WFTactics
/-- This tactic is used internally by lean before presenting the proof obligations from a well-founded
definition to the user via `decreasing_by`. It is not necessary to use this tactic manually.
 -/
tacticClean_wf : Lean.ParserDescr
-- Mathlib.Algebra.Group.Action.Defs
IsScalarTower.op_left : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
  [inst_3 : SMul M N] [inst_4 : SMul Mᵐᵒᵖ N] [IsCentralScalar M N] [inst_6 : SMul N α] [IsScalarTower M N α],
  IsScalarTower Mᵐᵒᵖ N α
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α}, a ∈ s → Prod.mk a ⁻¹' s ×ˢ t = t
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_factorization : ∀ (n : ℕ) [NeZero n],
  ArithmeticFunction.carmichael n = n.primeFactors.lcm fun p => ArithmeticFunction.carmichael (p ^ n.factorization p)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.mk_dest : ∀ {F : Type u → Type u} [q : QPF F] (x : QPF.Fix F), QPF.Fix.mk x.dest = x
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.divLeft₀_symm_apply : ∀ {G₀ : Type u_1} [inst : CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x : G₀),
  (Equiv.symm (Equiv.divLeft₀ a ha)) x = a / x
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- [Stacks Tag 0FX2](https://stacks.math.columbia.edu/tag/0FX2) (first part) -/
CategoryTheory.ObjectProperty.extensionProduct_retractClosure_retractClosure_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C),
  P.retractClosure.extensionProduct Q.retractClosure ≤ (P.extensionProduct Q).retractClosure
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The inverse of a square matrix, when it is invertible (and zero otherwise).  -/
Matrix.inv : {n : Type u'} → {α : Type v} → [Fintype n] → [DecidableEq n] → [CommRing α] → Inv (Matrix n n α)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.instIsProbabilityMeasureToMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω),
  MeasureTheory.IsProbabilityMeasure ↑μ
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} →
      {f : A ⟶ X} →
        {i : A ⟶ B} →
          {p : X ⟶ Y} →
            {g : B ⟶ Y} →
              {sq : CategoryTheory.CommSq f i p g} →
                (l : B ⟶ X) →
                  autoParam (CategoryTheory.CategoryStruct.comp i l = f)
                      CategoryTheory.CommSq.LiftStruct.fac_left._autoParam →
                    autoParam (CategoryTheory.CategoryStruct.comp l p = g)
                        CategoryTheory.CommSq.LiftStruct.fac_right._autoParam →
                      sq.LiftStruct
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
orthonormal_empty : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  Orthonormal 𝕜 fun x => ↑x
-- Mathlib.FieldTheory.Galois.Basic
/-- The subgroup fixing an intermediate field.  -/
IntermediateField.fixingSubgroup : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E → Subgroup Gal(E/F)
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- The legs of the cocone `coconeOfRepresentable` are natural in the choice of presheaf.  -/
CategoryTheory.Presheaf.coconeOfRepresentable_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.coconeOfRepresentable P₁).ι.app j) α =
    (CategoryTheory.Presheaf.coconeOfRepresentable P₂).ι.app ((CategoryTheory.CategoryOfElements.map α).op.obj j)
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.instOfNatCarrierOfNatNat : OfNat (↑TopCat.I) 0
-- Mathlib.NumberTheory.Real.Irrational
Nat.Prime.irrational_sqrt : ∀ {p : ℕ}, Nat.Prime p → Irrational √↑p
-- Lean.Elab.PreDefinition.TerminationMeasure
/-- Delaborates a `TerminationMeasure` back to a `TerminationHint`, e.g. for `termination_by?`.

This needs extra information:
* `arity` is the value arity of the recursive function
* `extraParams` indicates how many of the function's parameters are bound “after the colon”.
 -/
Lean.Elab.TerminationMeasure.delab : ℕ → ℕ → Lean.Elab.TerminationMeasure → Lean.MetaM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ),
  (p * Polynomial.X ^ n).degree = p.degree + ↑n
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_ne_nil_iff : ∀ {m n : ℕ}, (m<...n).toList ≠ [] ↔ m + 1 < n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofZeros_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).ι = CategoryTheory.CategoryStruct.id S.X₂
-- Init.Data.List.Basic
/-- Replaces the `n`th tail of `l` with the result of applying `f` to it. Returns the input without
using `f` if the index is larger than the length of the List.

Examples:
```lean example
["circle", "square", "triangle"].modifyTailIdx 1 List.reverse
```
```output
["circle", "triangle", "square"]
```
```lean example
["circle", "square", "triangle"].modifyTailIdx 1 (fun xs => xs ++ xs)
```
```output
["circle", "square", "triangle", "square", "triangle"]
```
```lean example
["circle", "square", "triangle"].modifyTailIdx 2 (fun xs => xs ++ xs)
```
```output
["circle", "square", "triangle", "triangle"]
```
```lean example
["circle", "square", "triangle"].modifyTailIdx 5 (fun xs => xs ++ xs)
```
```output
["circle", "square", "triangle"]
```
 -/
List.modifyTailIdx : {α : Type u} → List α → ℕ → (List α → List α) → List α
-- Mathlib.NumberTheory.FermatPsp
/-- All composite numbers are Fermat pseudoprimes to base 1.
 -/
Nat.fermatPsp_base_one : ∀ {n : ℕ}, 1 < n → ¬Nat.Prime n → n.FermatPsp 1
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.fieldEquivOfAlgEquivHom_injective : ∀ (A : Type u_8) (B : Type u_9) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (K : Type u_10)
  (L : Type u_11) [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : Algebra B L]
  [inst_7 : IsFractionRing A K] [inst_8 : IsFractionRing B L] [inst_9 : Algebra A L] [inst_10 : IsScalarTower A B L]
  [inst_11 : Algebra K L] [inst_12 : IsScalarTower A K L],
  Function.Injective ⇑(IsFractionRing.fieldEquivOfAlgEquivHom K L)
-- Mathlib.Data.Stream.Init
_private.Mathlib.Data.Stream.Init.0.Stream'.take.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → Stream' α → Sort u_2) →
    (x : ℕ) →
      (x_1 : Stream' α) → ((x : Stream' α) → motive 0 x) → ((n : ℕ) → (s : Stream' α) → motive n.succ s) → motive x x_1
-- Lean.Util.LeanOptions
Lean.instInhabitedLeanOptions.default : Lean.LeanOptions
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instDecidableEqOrdinal : DecidableEq Std.Time.Millisecond.Ordinal
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.ext_iff : ∀ {R : Type u} [inst : NonAssocRing R] {S T : Subring R}, S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
-- Batteries.Data.UnionFind.Basic
/-- Check whether two union-find nodes are equivalent, updating structure using path compression.  -/
Batteries.UnionFind.checkEquivN : {n : ℕ} → (self : Batteries.UnionFind) → Fin n → Fin n → n = self.size → Batteries.UnionFind × Bool
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is positive, the vectors are not equal.  -/
Orientation.ne_of_oangle_sign_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = 1 → x ≠ y
-- Mathlib.RingTheory.Unramified.Locus
Algebra.isOpen_unramifiedLocus : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.EssFiniteType R A], IsOpen (Algebra.unramifiedLocus R A)
-- Batteries.Data.Fin.Lemmas
Fin.findRev?_zero : ∀ {p : Fin 0 → Bool}, Fin.findRev? p = none
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.le_natDegree_of_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → n ≤ p.natDegree
-- Mathlib.Tactic.Linarith.Frontend
/-- Syntax for the arguments of `linarith`, after the optional `!`.  -/
Mathlib.Tactic.linarithArgsRest : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, deriv f y` equals `f b - f a`.  -/
intervalIntegral.integral_deriv_of_contDiffOn_uIcc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  ContDiffOn ℝ 1 f (Set.uIcc a b) → ∫ (x : ℝ) in a..b, deriv f x = f b - f a
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roo_eq_mkSlice_roo_min : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roo.Sliceable.mkSlice xs lo<...hi) =
    Std.Rco.Sliceable.mkSlice xs (min (lo + 1) (min hi xs.size))...min hi xs.size
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
Real.convergent.eq_def : ∀ (x : ℝ) (x_1 : ℕ),
  x.convergent x_1 =
    match x, x_1 with
    | ξ, 0 => ↑⌊ξ⌋
    | ξ, n.succ => ↑⌊ξ⌋ + ((Int.fract ξ)⁻¹.convergent n)⁻¹
-- Mathlib.Algebra.Group.Commutator
/-- The additive commutator of two elements `g₁` and `g₂`. This
is a scoped instance in the `commutatorElement` namespace to avoid clashing with other brackets  -/
addCommutatorElement : {G : Type u_1} → [AddGroup G] → Bracket G G
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
ordinaryHypergeometric.eq_1 : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) (x : 𝔸), ₂F₁ a b c x = (ordinaryHypergeometricSeries 𝔸 a b c).sum x
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.id_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  (X : CategoryTheory.InducedCategory D F),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_insert_self : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] (v : α) (t : RBTree.RBSet α cmp), v ∈ t.insert v
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_inv_div_log_sq_Ioi : ∀ {c : ℝ}, 1 < c → MeasureTheory.IntegrableOn (fun t => t⁻¹ / Real.log t ^ 2) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lift_apply : ∀ (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (X : Type u_9)
  (f : X → M) (g : X →₀ R), ((Finsupp.lift M R X) f) g = g.sum fun x r => r • f x
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
_private.Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Express the value of `sinZeta` at an odd integer `> 1` as a value of the Bernoulli polynomial.

Note that this formula is also correct for `k = 0` (i.e. for the value at `s = 1`), but we do not
prove it in this case, owing to the additional difficulty of working with series that are only
conditionally convergent.
 -/
HurwitzZeta.sinZeta_two_mul_nat_add_one : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.sinZeta (↑x) (2 * ↑k + 1) =
        (-1) ^ (k + 1) * (2 * ↑Real.pi) ^ (2 * k + 1) / 2 / ↑(2 * k + 1).factorial *
          Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
-- Init.Grind.Propagator
/-- A builtin propagator for the `grind` tactic.  -/
Lean.Parser.«command_Builtin_grind_propagator____:=_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) ⁻¹' Set.Icc b c = Set.Icc (b * a) (c * a)
-- Init.WFComputable
Acc.wfRel : {α : Sort u_1} → {r : α → α → Prop} → WellFoundedRelation { val // Acc r val }
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.mem_stabilizer_fixedSubmodule : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (e : V ≃ₗ[R] V),
  e ∈ MulAction.stabilizer (V ≃ₗ[R] V) (↑e).fixedSubmodule
-- Init.Internal.Order.Basic
Lean.Order.admissible_pi_apply : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.CCPO (β x)] (P : (x : α) → β x → Prop),
  (∀ (x : α), Lean.Order.admissible (P x)) → Lean.Order.admissible fun f => ∀ (x : α), P x (f x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.contains_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.contains k = t₂.contains k
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.erase : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α), m₁.Equiv m₂ → (m₁.erase k).Equiv (m₂.erase k)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.max!.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (x : α) → motive (some x)),
  (match none with
    | none => h_1 ()
    | some x => h_2 x) =
    h_1 ()
-- Mathlib.RingTheory.Ideal.Height
/-- In a nontrivial commutative ring `R`, the supremum of heights of all prime ideals is
equal to the Krull dimension of `R`.  -/
Ideal.sup_isPrime_height_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R], ↑(⨆ I, ⨆ (_ : I.IsPrime), I.height) = ringKrullDim R
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.coeffs_q_subset : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B)
  (i : Algebra.Smooth.DescentAux.vars✝ D),
  ↑(Algebra.Smooth.DescentAux.q✝ D i).coeffs ⊆
    Set.range ⇑(MvPolynomial.map (algebraMap (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) A))
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_lieSpan : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L} {x : L},
  x ∈ LieSubalgebra.lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying `MulHom`.  -/
MagmaCat.Hom.hom' : {A B : MagmaCat} → A.Hom B → ↑A →ₙ* ↑B
-- Mathlib.Data.List.MinMax
List.argmax_eq_none : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {l : List α},
  List.argmax f l = none ↔ l = []
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff m₂ ⋯).getKey? k = none
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w curr : ℕ} {aig : Std.Sat.AIG α} {cin : aig.Ref}
  {lhs rhs : aig.RefVec w},
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls.size
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The action of a pair of maps `f : c ⟶ c'` and `d ⟶ d'`. By default,
this is defined in terms of `actionHomLeft` and `actionHomRight`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom : {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} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] →
            {c c' : C} →
              {d d' : D} →
                (c ⟶ c') →
                  (d ⟶ d') →
                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶
                      CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d')
-- Mathlib.GroupTheory.Commutator.Basic
commutator_mem_commutatorSet : ∀ {G : Type u_1} [inst : Group G] (g₁ g₂ : G), ⁅g₁, g₂⁆ ∈ commutatorSet G
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.parallel_comm : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁.Parallel s₂ ↔ s₂.Parallel s₁
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_of_ne : ∀ {n m : ℕ}, n ≠ m → (2 ^ n).testBit m = false
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.pure : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Monad m] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  {α : Type u} {pre : Pred} {post : α → Pred} {epost : EPred} (a : α),
  Lean.Order.PartialOrder.rel pre (post a) → ⦃ pre ⦄ pure a ⦃ post; epost ⦄
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instIsAffineObjOppositeCommRingCatSchemeSpec : ∀ (R : CommRingCatᵒᵖ), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.Spec.obj R)
-- Mathlib.Algebra.Order.Star.Basic
IsStarProjection.one_sub_nonneg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {p : R},
  IsStarProjection p → 0 ≤ 1 - p
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R), (γ.smul a).φQ = a • γ.φQ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k a : α} {v : β}, (t.insert k v)[a]! = if cmp k a = Ordering.eq then v else t[a]!
-- Mathlib.Algebra.Group.Basic
natAbs_nsmul_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a : G} {n : ℤ}, n.natAbs • a = 0 ↔ n • a = 0
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.algebraMap_quotient_map_quotient : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {p : Ideal R} [inst_2 : Algebra R S] (x : R),
  (algebraMap (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk p) x) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) x)
-- Mathlib.Algebra.Polynomial.Coeff
/-- **Alias** of `Polynomial.finsetSum_coeff`. -/
Polynomial.finset_sum_coeff : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ),
  (∑ b ∈ s, f b).coeff n = ∑ b ∈ s, (f b).coeff n
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.coe_of : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : CompactSpace G] [inst_4 : TotallyDisconnectedSpace G], ↑(ProfiniteAddGrp.of G).toProfinite.toTop = G
-- Mathlib.Algebra.Ring.Defs
Ring.toAddCommGroup : {R : Type u} → [self : Ring R] → AddCommGroup R
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.addActionFinset.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddMonoid α] [inst_2 : AddAction α β],
  Finset.addActionFinset = Function.Injective.addAction SetLike.coe ⋯ ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.map_tprod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.NeBot] [inst_3 : CommMonoid γ] [inst_4 : TopologicalSpace γ] [T2Space γ],
  Multipliable f L →
    ∀ {G : Type u_4} [inst_6 : FunLike G α γ] [MonoidHomClass G α γ] (g : G),
      Continuous ⇑g → g (∏'[L] (i : β), f i) = ∏'[L] (i : β), g (f i)
-- Mathlib.NumberTheory.Height.NumberField
/-- The term corresponding to a finite place in the definition of the multiplicative height
of a tuple of rational numbers equals `1` if the tuple consists of coprime integers.  -/
Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_one : ∀ {ι : Type u_1} [inst : Fintype ι] [Nonempty ι] {x : ι → ℤ} (v : NumberField.FinitePlace ℚ),
  Finset.univ.gcd x = 1 → ⨆ i, v ↑(x i) = 1