mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Field.Basic
/-- Pullback a `Field` along an injective function.  -/
Function.Injective.field : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Zero K] →
      [inst_1 : Add K] →
        [inst_2 : Neg K] →
          [inst_3 : Sub K] →
            [inst_4 : One K] →
              [inst_5 : Mul K] →
                [inst_6 : Inv K] →
                  [inst_7 : Div K] →
                    [inst_8 : SMul ℕ K] →
                      [inst_9 : SMul ℤ K] →
                        [inst_10 : SMul ℚ≥0 K] →
                          [inst_11 : SMul ℚ K] →
                            [inst_12 : Pow K ℕ] →
                              [inst_13 : Pow K ℤ] →
                                [inst_14 : NatCast K] →
                                  [inst_15 : IntCast K] →
                                    [inst_16 : NNRatCast K] →
                                      [inst_17 : RatCast K] →
                                        (f : K → L) →
                                          Function.Injective f →
                                            [inst_18 : Field L] →
                                              f 0 = 0 →
                                                f 1 = 1 →
                                                  (∀ (x y : K), f (x + y) = f x + f y) →
                                                    (∀ (x y : K), f (x * y) = f x * f y) →
                                                      (∀ (x : K), f (-x) = -f x) →
                                                        (∀ (x y : K), f (x - y) = f x - f y) →
                                                          (∀ (x : K), f x⁻¹ = (f x)⁻¹) →
                                                            (∀ (x y : K), f (x / y) = f x / f y) →
                                                              (∀ (n : ℕ) (x : K), f (n • x) = n • f x) →
                                                                (∀ (n : ℤ) (x : K), f (n • x) = n • f x) →
                                                                  (∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) →
                                                                    (∀ (q : ℚ) (x : K), f (q • x) = q • f x) →
                                                                      (∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                                        (∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) →
                                                                          (∀ (n : ℕ), f ↑n = ↑n) →
                                                                            (∀ (n : ℤ), f ↑n = ↑n) →
                                                                              (∀ (q : ℚ≥0), f ↑q = ↑q) →
                                                                                (∀ (q : ℚ), f ↑q = ↑q) → Field K
-- Mathlib.Data.Multiset.AddSub
Multiset.sub_add_eq_sub_sub : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s - (t + u) = s - t - u
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y),
  ∃ g,
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X) g =
      CategoryTheory.CategoryStruct.comp f (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj Y)
-- Mathlib.Topology.Order.LiminfLimsup
Antitone.limsup_nhdsLT_eq_iInf₂ : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β} [NoMinOrder α],
  Antitone f → ∀ (a : α), Filter.limsup f (nhdsWithin a (Set.Iio a)) = ⨅ r, ⨅ (_ : r < a), f r
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Array containing the basic variables' indexes  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.basic : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType → Array ℕ
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.InftyValuation.map_add_le_max'`. -/
FunctionField.InftyValuation.map_add_le_max' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] (x y : RatFunc F),
  RatFunc.inftyValuationDef F (x + y) ≤ max (RatFunc.inftyValuationDef F x) (RatFunc.inftyValuationDef F y)
-- Mathlib.Data.List.Pi
List.mem_pi : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Type u_2} {l : List ι} (fs : (i : ι) → List (α i))
  (f : (i : ι) → i ∈ l → α i), f ∈ l.pi fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_neg'`.  -/
Right.add_neg' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b : α}, a < 0 → b < 0 → a + b < 0
-- Mathlib.Algebra.Field.Subfield.Defs
/-- The underlying `AddSubgroup` of a subfield.  -/
Subfield.toAddSubgroup : {K : Type u} → [inst : DivisionRing K] → Subfield K → AddSubgroup K
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.dropEndWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.dropEndWhile pat = s.sliceTo (s.skipSuffixWhile pat)
-- Lean.Elab.Term.TermElabM
/-- Applies the given transformation to the `TacticFinishedSnapshot`.  -/
Lean.Elab.Tactic.TacticFinishedSnapshot.transform : Lean.Elab.Tactic.TacticFinishedSnapshot → Lean.Language.SnapshotTreeTransform → Lean.Elab.Tactic.TacticFinishedSnapshot
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.triangleOpEquivalence_counitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ],
  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).counitIso =
    CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr.congr_simp : ∀ {α : Type u_1} {β : Type v} (f f_1 : α → β → β) (e_f : f = f_1) [inst : LeftCommutative f] (b b_1 : β),
  b = b_1 → ∀ (s s_1 : Multiset α), s = s_1 → Multiset.foldr f b s = Multiset.foldr f_1 b_1 s_1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.prependMapGE : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Std.DTreeMap.Internal.Zipper α β → Std.DTreeMap.Internal.Zipper α β
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.finrank_eq_max_natDegree : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K),
  Module.finrank (↥K⟮f⟯) (RatFunc K) = max f.num.natDegree f.denom.natDegree
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- The type of morphisms in `CommHopfAlgCat R`.  -/
CommHopfAlgCat.Hom : {R : Type u} → [inst : CommRing R] → CommHopfAlgCat R → CommHopfAlgCat R → Type v
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ)
  {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g)))
-- Mathlib.Logic.Function.Basic
/-- Uncurrying operator. The most generic use is to recursively uncurry. For instance
`f : α → β → γ → δ` will be turned into `↿f : α × β × γ → δ`. One can also add instances
for bundled maps.  -/
Function.«term↿_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.one_minus_lt_one : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] (x : ↑(Set.Ioo 0 1)), 1 - ↑x < 1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.trans_right : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  t₁.Bounded o₁ ↑x → t₂.Bounded (↑x) o₂ → t₁.Bounded o₁ o₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.compare_get?_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.get? k) = true
-- Mathlib.NumberTheory.PrimeCounting
Nat.monotone_primeCounting' : Monotone Nat.primeCounting'
-- Mathlib.Topology.MetricSpace.Defs
dist_ne_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y ≠ 0 ↔ x ≠ y
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
_private.Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer.0.LinearMap.exists_restrict_span_singleton_eq_smul_id : ∀ {R : Type u_3} {V : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {v : V}
  {A : V →ₗ[R] V},
  A v ∈ R ∙ v → ∃ c, A v = c • v ∧ ∃ (hcomap : R ∙ v ≤ Submodule.comap A (R ∙ v)), A.restrict hcomap = c • LinearMap.id
-- Std.Http.Data.URI.Basic
Std.Http.instInhabitedRequestTarget : Inhabited Std.Http.RequestTarget
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_union : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
  (s₁ s₂ : Set α), omegaLimit f ϕ (s₁ ∪ s₂) = omegaLimit f ϕ s₁ ∪ omegaLimit f ϕ s₂
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.modify_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {k : α} {f : β k → β k}, m.modify k f = ↑(Std.DHashMap.Internal.Raw₀.modify ⟨m, ⋯⟩ k f)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.modifier.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.modifier = 1
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.card_isConj_mul_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial) =
    (Fintype.card α).factorial
-- Mathlib.Data.List.Forall2
List.tail_sublistForall₂_self : ∀ {α : Type u_1} {Rₐ : α → α → Prop} [Std.Refl Rₐ] (l : List α), List.SublistForall₂ Rₐ l.tail l
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instValued : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Valued (WithVal v) Γ₀
-- Mathlib.Algebra.Group.Subgroup.Basic
IsConj.normalClosure_eq_top_of : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N} {hg' : g' ∈ N},
  IsConj g g' → Subgroup.normalClosure {⟨g, hg⟩} = ⊤ → Subgroup.normalClosure {⟨g', hg'⟩} = ⊤
-- Init.Data.Rat.Lemmas
Rat.instCommutativeHAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le : ∀ {F : Type u_2} {α : outParam (Type u_3)} {inst : FunLike F (Set α) ENNReal}
  [self : MeasureTheory.OuterMeasureClass F α] (f : F) (s : ℕ → Set α),
  Pairwise (Function.onFun Disjoint s) → f (⋃ i, s i) ≤ ∑' (i : ℕ), f (s i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀),
  E.presieve₀ (E.f i)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Add-sub-sub version.  -/
Finset.ruzsa_triangle_inequality_add_sub_sub : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] (A B C : Finset G),
  (A + C).card * B.card ≤ (A - B).card * (B - C).card
-- Mathlib.Data.List.MinMax
_private.Mathlib.Data.List.MinMax.0.List.foldl_argAux_mem : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (l : List α) (a m : α),
  m ∈ List.foldl (List.argAux r) (some a) l → m ∈ a :: l
-- Init.Internal.Order.Basic
Lean.Order.CompleteLattice.toPartialOrder : {α : Sort u} → [self : Lean.Order.CompleteLattice α] → Lean.Order.PartialOrder α
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.toSub : {α : Type u} → [self : Lean.Grind.Ring α] → Sub α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- This is a helper construction that can be useful when verifying that a category has certain wide
equalizers. Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
`parallelFamily (fun j ↦ F.map (line j))`, and a trident on `fun j ↦ F.map (line j)`,
we get a cone on `F`.

If you're thinking about using this, have a look at
`hasWideEqualizers_of_hasLimit_parallelFamily`, which you may find to be an easier way of
achieving your goal.  -/
CategoryTheory.Limits.Cone.ofTrident : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} →
        (CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) →
          CategoryTheory.Limits.Cone F
-- 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.convAbel! : Lean.ParserDescr
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.match_1.splitter : (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) →
  (x : ByteArray.utf8DecodeChar?.FirstByte) →
    (x = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive ByteArray.utf8DecodeChar?.FirstByte.invalid) →
      (x = ByteArray.utf8DecodeChar?.FirstByte.done → motive ByteArray.utf8DecodeChar?.FirstByte.done) →
        (x = ByteArray.utf8DecodeChar?.FirstByte.oneMore → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore) →
          (x = ByteArray.utf8DecodeChar?.FirstByte.twoMore → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore) →
            (x = ByteArray.utf8DecodeChar?.FirstByte.threeMore → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore) →
              motive x
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.LeftUnitorBimod.inv_hom_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S),
  CategoryTheory.CategoryStruct.comp (Bimod.LeftUnitorBimod.inv P) (Bimod.LeftUnitorBimod.hom P) =
    CategoryTheory.CategoryStruct.id P.X
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
GenContFract.of_isSimpContFract : ∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K],
  (GenContFract.of v).IsSimpContFract
-- Mathlib.LinearAlgebra.PID
/-- If a linear endomorphism of a (finite, free) module `M` takes values in a submodule `p ⊆ M`,
then the trace of its restriction to `p` is equal to its trace on `M`.  -/
LinearMap.trace_restrict_eq_of_forall_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Module.Free R M] [IsDomain R] [IsPrincipalIdealRing R] (p : Submodule R M) (f : M →ₗ[R] M) (hf : ∀ (x : M), f x ∈ p)
  (hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯), (LinearMap.trace R ↥p) (f.restrict hf') = (LinearMap.trace R M) f
-- Mathlib.Algebra.Ring.Ext
CommSemiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : CommSemiring R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceFrom_ne_startPos : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos},
  p ≠ (s.sliceFrom p₀).startPos → String.Slice.Pos.ofSliceFrom p ≠ s.startPos
-- Mathlib.Order.Preorder.Finite
/-- A strictly monotone self-map of a finite linear order fixes every point.  -/
StrictMono.apply_eq : ∀ {α : Type u_4} [inst : LinearOrder α] [Finite α] {f : α → α} {x : α}, StrictMono f → f x = x
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.eqOn_Ioc_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X]
  {m : MeasurableSpace X} [inst_3 : TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  [DenselyOrdered X] {a b : X} {f g : X → Y},
  f =ᵐ[μ.restrict (Set.Ioc a b)] g →
    ContinuousOn f (Set.Ioc a b) → ContinuousOn g (Set.Ioc a b) → Set.EqOn f g (Set.Ioc a b)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_inv_cancel_right : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α}, IsUnit b → ∀ (a : α), a * b * b⁻¹ = a
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f : R[X]`. Let `s` be a finite index set.
Let `g i` be a collection of monic and pairwise coprime polynomials indexed by `s`,
and for each `g i` let `n i` be a natural number.
Let `K` be an algebra over `R[X]` containing inverses `gi i` for each `g i`.
Then a fraction of the form `f * ∏ i ∈ s, gi i ^ n i` can be rewritten as
`q + ∑ i ∈ s, ∑ j : Fin (n i), r i j * gi i ^ (j + 1)`, where `degree (r i j) < degree (g i)`.
See `mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse` for the
uniqueness of this representation.  -/
Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : CommRing K] [inst_2 : Algebra (Polynomial R) K]
  [Nontrivial R] {ι : Type u_3} {s : Finset ι} (f : Polynomial R) {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ (n : ι → ℕ) {gi : ι → K},
        (∀ i ∈ s, gi i * (algebraMap (Polynomial R) K) (g i) = 1) →
          ∃ q r,
            (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
              (algebraMap (Polynomial R) K) f * ∏ i ∈ s, gi i ^ n i =
                (algebraMap (Polynomial R) K) q + ∑ i ∈ s, ∑ j, (algebraMap (Polynomial R) K) (r i j) * gi i ^ (↑j + 1)
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_filter : ∀ {α : Type u_1} {β : Type v} (p : α → Prop) [inst : DecidablePred p] (f : α → Option β) (s : Multiset α),
  Multiset.filterMap f (Multiset.filter p s) = Multiset.filterMap (fun x => if p x then f x else none) s
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y)
  {Z : D} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf.fst g) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (F.map (hf.snd g)) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Data.ENat.Basic
ENat.toNat_add : ∀ {m n : ℕ∞}, m ≠ ⊤ → n ≠ ⊤ → (m + n).toNat = m.toNat + n.toNat
-- Mathlib.Order.RelSeries
RelSeries.smash_length : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : p.last = q.head),
  (p.smash q connect).length = p.length + q.length
-- Std.Async.Signal
Std.Async.Signal.sigxfsz.sizeOf_spec : sizeOf Std.Async.Signal.sigxfsz = 1
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrameCoeff.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] (i : ι), Bundle.Trivialization.localFrameCoeff I e b i = ⋯.coeff i
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_zero : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B], ⇑0 = 0
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0),
  R.extMk f m hm hf =
    R.extEquivCohomologyClass.symm
      (CochainComplex.HomComplex.CohomologyClass.mk
        (CochainComplex.HomComplex.Cocycle.fromSingleMk
          (CategoryTheory.CategoryStruct.comp f (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
-- Mathlib.Data.Finset.Grade
/-- Finsets form an order-connected suborder of sets.  -/
Finset.ordConnected_range_coe : ∀ {α : Type u_1}, (Set.range SetLike.coe).OrdConnected
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.H = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Algebra.Algebra.Basic
algebra_compatible_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M] (r : R) (m : M),
  r • m = (algebraMap R A) r • m
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.liftFromOverComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {X : C}
  {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {F : CategoryTheory.Functor C D}
  (x : CategoryTheory.WithTerminal J),
  CategoryTheory.WithTerminal.liftFromOverComp.hom.app x =
    match x with
    | CategoryTheory.WithTerminal.star =>
      CategoryTheory.CategoryStruct.id
        ((CategoryTheory.WithTerminal.liftFromOver.obj (K.comp (CategoryTheory.Over.post F))).obj
          CategoryTheory.WithTerminal.star)
    | CategoryTheory.WithTerminal.of a =>
      CategoryTheory.CategoryStruct.id
        ((CategoryTheory.WithTerminal.liftFromOver.obj (K.comp (CategoryTheory.Over.post F))).obj
          (CategoryTheory.WithTerminal.of a))