mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Num.Lemmas
Num.castNum_eq_bitwise : ∀ {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num),
  g false false = false →
    f 0 0 = 0 →
      (∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0) →
        (∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0) →
          (∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n) →
            (p 1 1 = bif g true true then 1 else 0) →
              (∀ (b : Bool) (n : PosNum),
                  p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0)) →
                (∀ (a : Bool) (m : PosNum),
                    p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0)) →
                  (∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)) →
                    ∀ (m n : Num), ↑(f m n) = Nat.bitwise g ↑m ↑n
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  {c : NNReal}, (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.Indep.eq_union_image_of_disjointSum : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E} {I : Set α},
  (M.disjointSum N h).Indep I → ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n},
  φ.IsQF →
    P ⊥ →
      (∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) →
        (∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) →
          (∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) →
            (∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ
-- Mathlib.AlgebraicGeometry.Normalization
/-- The uniqueness part of the universal property for relative normalization.
Suppose `f : X ⟶ Y` is qcqs and factors into `X ⟶ T ⟶ Y` with `T ⟶ Y` affine, then
there is at most one map `f.normalization ⟶ T` that commutes with them.  -/
AlgebraicGeometry.Scheme.Hom.normalization.hom_ext : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme}
  (f₁ f₂ : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ T) (g : T ⟶ Y) [AlgebraicGeometry.IsAffineHom g],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) f₁ =
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) f₂ →
    CategoryTheory.CategoryStruct.comp f₁ g = AlgebraicGeometry.Scheme.Hom.fromNormalization f →
      CategoryTheory.CategoryStruct.comp f₂ g = AlgebraicGeometry.Scheme.Hom.fromNormalization f → f₁ = f₂
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [inst_2 : DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLE α] →
            {n : Type u → Type w} →
              [Monad n] →
                (γ : Type u) →
                  (Pl : α → γ → ForInStep γ → Prop) →
                    Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl →
                      (LargeEnough : α → Prop) →
                        (∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) →
                          (upperBound : α) →
                            γ →
                              (next : α) →
                                LargeEnough next →
                                  ((out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n { s // Pl out c s }) →
                                    n γ
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.one_div_nonneg : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 ≤ 1 / p
-- Init.Data.Nat.Lemmas
Nat.eq_div_of_mul_eq_right : ∀ {c a b : ℕ}, c ≠ 0 → c * a = b → a = b / c
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The isomorphism `S ⧸ pS ≃+* Sₚ ⧸ p·Sₚ`, where `Sₚ` is the localization of `S` at the (image) of
the complement of `p`
 -/
IsLocalization.AtPrime.equivQuotientMapMaximalIdeal : (S : Type u_6) →
  {R : Type u_7} →
    [inst : CommRing R] →
      (p : Ideal R) →
        [inst_1 : p.IsMaximal] →
          (Rₚ : Type u_8) →
            [inst_2 : CommRing Rₚ] →
              [inst_3 : Algebra R Rₚ] →
                [IsLocalization.AtPrime Rₚ p] →
                  [inst_5 : IsLocalRing Rₚ] →
                    (Sₚ : Type u_9) →
                      [inst_6 : CommRing S] →
                        [inst_7 : Algebra R S] →
                          [inst_8 : CommRing Sₚ] →
                            [inst_9 : Algebra S Sₚ] →
                              [inst_10 : Algebra R Sₚ] →
                                [inst_11 : Algebra Rₚ Sₚ] →
                                  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] →
                                    [IsScalarTower R S Sₚ] →
                                      [IsScalarTower R Rₚ Sₚ] →
                                        S ⧸ Ideal.map (algebraMap R S) p ≃+*
                                          Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ)
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Option.getBool : Lean.Options → Lean.Name → Bool → Bool
-- Mathlib.RingTheory.Kaehler.Basic
/-- This is a special case of `kerTotal_map` where `R = S`.
The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/R}` is spanned by the image of the
kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `da` with `a : A`.
 -/
KaehlerDifferential.kerTotal_map' : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B],
  Function.Surjective ⇑(algebraMap A B) →
    Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B))
        (KaehlerDifferential.kerTotal R A ⊔ Submodule.span A (Set.range fun x => fun₀ | (algebraMap R A) x => 1)) =
      Submodule.restrictScalars A (KaehlerDifferential.kerTotal R B)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_tsub : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)] (f g : Π₀ (i : ι), α i), ⇑(f - g) = ⇑f - ⇑g
-- Init.Conv
/-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:
* `enter [i]` is equivalent to `arg i`.
* `enter [@i]` is equivalent to `arg @i`.
* `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
* `enter [in e]` (where `e` is a term) is equivalent to `pattern e`.
  Occurrences can be specified with `enter [in (occs := ...) e]`.
For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
will traverse to the subterm `b`.  -/
Lean.Parser.Tactic.Conv.enter : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- A subgroup of `GL(2, ℝ)` is arithmetic if it is commensurable with the image of `SL(2, ℤ)`.  -/
Subgroup.IsArithmetic : Subgroup (GL (Fin 2) ℝ) → Prop
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.mk_eq_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] (v : Module.Basis ι R M),
  Cardinal.lift.{v, w} (Cardinal.mk ι) = Cardinal.lift.{w, v} (Module.rank R M)
-- Mathlib.CategoryTheory.Sites.Point.Category
/-- A morphism between points of a site consists of a morphism
between the functors `Point.fiber`, in the opposite direction.  -/
CategoryTheory.GrothendieckTopology.Point.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → J.Point → J.Point → Type (max u w)
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioi_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : Fintype β] [inst_4 : LocallyFiniteOrderTop β] (a : α),
  Finset.Ioi (Sum.inlₗ a) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum Finset.univ)
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableWithRpcRefOfTypeName : {α : Type} → [TypeName α] → Lean.Server.RpcEncodable (Lean.Server.WithRpcRef α)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Given a set `s`, return the continuous linear map `fun x => μ.real s • x`. The extension
of that set function through `setToL1` gives the Bochner integral of L1 functions.  -/
MeasureTheory.weightedSMul : {α : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [inst_1 : NormedSpace ℝ F] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Set α → F →L[ℝ] F
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.foldM_eq_forIn : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad n] [inst_3 : Std.IteratorLoop α m n] [inst_4 : MonadLiftT m n] {f : γ → β → n γ} {init : γ}
  {it : Std.IterM m β}, Std.IterM.foldM f init it = forIn it init fun x acc => ForInStep.yield <$> f acc x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_interval_sub_interval_comm : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c d : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable f μ c d →
      IntervalIntegrable f μ a c →
        ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ - ∫ (x : ℝ) in b..d, f x ∂μ
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A countable product of completely metrizable spaces is completely metrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable : ∀ {ι : Type u_3} [Countable ι] {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), TopologicalSpace.IsCompletelyMetrizableSpace (X i)],
  TopologicalSpace.IsCompletelyMetrizableSpace ((i : ι) → X i)
-- Mathlib.Algebra.Free
/-- The tail of the element  -/
FreeAddSemigroup.tail : {α : Type u} → FreeAddSemigroup α → List α
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.toAdditive_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : MulOneClass H] (f : G ≃* H) (a : Additive H),
  (MulEquiv.toAdditive f).symm a = (MonoidHom.toAdditive f.symm.toMonoidHom) a
-- Mathlib.LinearAlgebra.Eigenspace.Pi
Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) [IsDomain R] [Module.IsTorsionFree R M],
  (∀ (i j : ι) (φ : R), Set.MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
    iSupIndep fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
-- Mathlib.FieldTheory.Normal.Closure
AlgHom.fieldRange_le_normalClosure : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] (f : K →ₐ[F] L), f.fieldRange ≤ IntermediateField.normalClosure F K L
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.reverseAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) → ((r : List α) → motive [] r) → ((a : α) → (l r : List α) → motive (a :: l) r) → motive x x_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List ((a : α) × β a)}, (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : HomotopyCategory C (ComplexShape.up ℤ)} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj L) (a a' : ℤ)
  (h : autoParam (n + a = a') DerivedCategory.shiftMap_homologyFunctor_map_Qh._auto_1) {Z : C}
  (h_1 : ((DerivedCategory.homologyFunctor C 0).shift a').obj (DerivedCategory.Qh.obj L) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((DerivedCategory.homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f DerivedCategory.Qh) a a' h) h_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactorsh C a).hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
          ((DerivedCategory.homologyFunctorFactorsh C a').inv.app L)))
      h_1
-- Mathlib.Tactic.FunProp.Types
/-- Name of the origin.  -/
Mathlib.Meta.FunProp.Origin.name : Mathlib.Meta.FunProp.Origin → Lean.Name
-- Mathlib.Data.Finset.NatAntidiagonal
/-- The cardinality of the antidiagonal of `n` is `n + 1`.  -/
Finset.Nat.card_antidiagonal : ∀ (n : ℕ), (Finset.HasAntidiagonal.antidiagonal n).card = n + 1
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp_of_model : ∀ {K : Type u_2} [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K]
  [inst_5 : FirstOrder.Ring.CompatibleRing K] [K ⊨ FirstOrder.Language.Theory.field] (ax : FirstOrder.Field.FieldAxiom),
  FirstOrder.Field.FieldAxiom.toProp K ax
-- Init.Data.String.Defs
/-- Adds multiple repetitions of a character to the end of a string.

Returns `s`, with `n` repetitions of `c` at the end. Internally, the implementation repeatedly calls
`String.push`, so the string is modified in-place if there is a unique reference to it.

Examples:
 * `"indeed".pushn '!' 2 = "indeed!!"`
 * `"indeed".pushn '!' 0 = "indeed"`
 * `"".pushn ' ' 4 = "    "`
 -/
String.pushn : String → Char → ℕ → String
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target_union_compl_range_mem_nhds_of_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {y : E} {x : M},
  y ∈ (extChartAt I x).target → (extChartAt I x).target ∪ (Set.range ↑I)ᶜ ∈ nhds y
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instLocalization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid S)
  [Algebra.QuasiFinite R S], Algebra.QuasiFinite R (Localization M)
-- Mathlib.Analysis.Complex.HasPrimitives
Complex.IsExactOn.differentiableOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {U : Set ℂ},
  IsOpen U → Complex.IsExactOn f U → DifferentiableOn ℂ f U
-- Mathlib.Tactic.Linter.HaveLetLinter
/-- returns the `have` syntax whose corresponding hypothesis does not have Type `Prop` and
also a `Format`ted version of the corresponding Type.  -/
Mathlib.Linter.haveLet.nonPropHaves : Lean.Elab.InfoTree → Lean.Elab.Command.CommandElabM (Array (Lean.Syntax × Std.Format))
-- Mathlib.Tactic.Linter.DocString
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.getDeclModifiers.match_1.eq_2 : ∀ (motive : Lean.Syntax → Sort u_1) (x : Lean.Syntax)
  (h_1 :
    (s : Lean.Syntax) →
      (info : Lean.SourceInfo) →
        (kind : Lean.SyntaxNodeKind) →
          (args : Array Lean.Syntax) → s = Lean.Syntax.node info kind args → motive (Lean.Syntax.node info kind args))
  (h_2 : (x : Lean.Syntax) → motive x),
  (∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
      x = Lean.Syntax.node info kind args → False) →
    (match x with
      | s@h:(Lean.Syntax.node info kind args) => h_1 s info kind args h
      | x => h_2 x) =
      h_2 x
-- Mathlib.Data.Multiset.Count
Multiset.countP_le_card : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α), Multiset.countP p s ≤ s.card
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.abelNF : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.val_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (x : ↥S), S.val x = ↑x
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_symm_leadingCoeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ),
  (HahnSeries.addOppositeEquiv.symm x).leadingCoeff = AddOpposite.op (AddOpposite.unop x).leadingCoeff
-- Mathlib.Tactic.Linter.FindDeprecations
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.mk.injEq : ∀ (module decl : Lean.Name) (rgStart rgStop : Lean.Position) (since : String) (module_1 decl_1 : Lean.Name)
  (rgStart_1 rgStop_1 : Lean.Position) (since_1 : String),
  ({ module := module, decl := decl, rgStart := rgStart, rgStop := rgStop, since := since } =
      { module := module_1, decl := decl_1, rgStart := rgStart_1, rgStop := rgStop_1, since := since_1 }) =
    (module = module_1 ∧ decl = decl_1 ∧ rgStart = rgStart_1 ∧ rgStop = rgStop_1 ∧ since = since_1)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.υ_inv_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.υ hF).inv.app X =
    CategoryTheory.CategoryStruct.comp (e'.inverse.map (hF.inv.app X)) (e'.unitIso.inv.app (eA.functor.obj X))
-- Init.Data.Array.Lemmas
Array.eq_replicate_of_mem : ∀ {α : Type u_1} {a : α} {xs : Array α}, (∀ b ∈ xs, b = a) → xs = Array.replicate xs.size a
-- Init.Data.Array.Lemmas
Array.findRevM?_eq_findM?_reverse : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {f : α → m Bool} {xs : Array α},
  Array.findRevM? f xs = Array.findM? f xs.reverse
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mrange_inl_sup_mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange Monoid.Coprod.inl ⊔ MonoidHom.mrange Monoid.Coprod.inr = ⊤
-- Init.Data.Array.Lemmas
Array.size_pos_iff : ∀ {α : Type u_1} {xs : Array α}, 0 < xs.size ↔ xs ≠ #[]
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C),
  CategoryTheory.IsSeparator G → (CategoryTheory.preadditiveCoyonedaObj G).PreservesInjectiveObjects
-- Mathlib.Data.Nat.Squarefree
Nat.factorization_eq_one_of_squarefree : ∀ {n p : ℕ}, Squarefree n → Nat.Prime p → p ∣ n → n.factorization p = 1
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.irreducible_aux1 : ∀ {p : Polynomial ℤ} {k m n : ℕ},
  k < m →
    m < n →
      ∀ (u v w : ℤˣ),
        p = Polynomial.trinomial k m n ↑u ↑v ↑w →
          Polynomial.C ↑v *
              (Polynomial.C ↑u * Polynomial.X ^ (m + n) + Polynomial.C ↑w * Polynomial.X ^ (n - m + k + n)) =
            {
              toFinsupp :=
                AddMonoidAlgebra.ofCoeff
                  (Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp.coeff) }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The set of accessible `Λ'.write` machine states.  -/
Turing.TM1to1.writes : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → [Fintype Γ] → Turing.TM1.Stmt Γ Λ σ → Finset (Turing.TM1to1.Λ' Γ Λ σ)
-- Mathlib.Logic.IsEmpty.Defs
Sigma.isEmpty_left : ∀ {α : Type u_1} [IsEmpty α] {E : α → Type v}, IsEmpty (Sigma E)
-- Mathlib.Algebra.Group.Defs
ofNat_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G) (n : ℕ), OfNat.ofNat n • a = OfNat.ofNat n • a
-- Mathlib.Data.PNat.Basic
instAddLeftReflectLTPNat : AddLeftReflectLT ℕ+
-- Mathlib.Analysis.Fourier.ZMod
/-- The discrete Fourier transform on `ℤ / N ℤ` (with the counting measure), bundled as a linear
equivalence. Denoted as `𝓕` within the `ZMod` namespace.
 -/
ZMod.term𝓕 : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Composing `f : Lp` with `L : E →L[𝕜] F`.  -/
ContinuousLinearMap.compLp : {α : Type u_1} →
  {E : Type u_4} →
    {F : Type u_5} →
      {m : MeasurableSpace α} →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedAddCommGroup F] →
                {𝕜 : Type u_6} →
                  {𝕜' : Type u_7} →
                    [inst_2 : NontriviallyNormedField 𝕜] →
                      [inst_3 : NontriviallyNormedField 𝕜'] →
                        [inst_4 : NormedSpace 𝕜 E] →
                          [inst_5 : NormedSpace 𝕜' F] →
                            {σ : 𝕜 →+* 𝕜'} →
                              [RingHomIsometric σ] →
                                (E →SL[σ] F) → ↥(MeasureTheory.Lp E p μ) → ↥(MeasureTheory.Lp F p μ)
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.forIn'.loop.match_3.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace x w =
    x ↑w - (↑(↑w).mult * ∑ w', x w') * (↑(Module.finrank ℚ K))⁻¹
-- Mathlib.Data.Fintype.Sets
Fintype.finsetEquivSet.eq_1 : ∀ {α : Type u_1} [inst : Fintype α],
  Fintype.finsetEquivSet = { toFun := SetLike.coe, invFun := fun s => s.toFinset, left_inv := ⋯, right_inv := ⋯ }