mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ (r r_1 : ℕ),
      r = r_1 →
        ∀ (k k_1 : ℕ),
          k = k_1 →
            ∀ (v v_1 : α),
              v = v_1 →
                ∀ (w₁ w₁_1 : α),
                  w₁ = w₁_1 →
                    ∀ (w₂ w₂_1 : α),
                      w₂ = w₂_1 →
                        ∀ (s s_1 : Finset α),
                          s = s_1 →
                            ∀ (t t_1 : Finset α),
                              t = t_1 →
                                G.IsFiveWheelLike r k v w₁ w₂ s t = G_1.IsFiveWheelLike r_1 k_1 v_1 w₁_1 w₂_1 s_1 t_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.π_map_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) {Z : ModuleCat k} (h : groupHomology B n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A n)
      (CategoryTheory.CategoryStruct.comp (groupHomology.map f φ n) h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ n)
      (CategoryTheory.CategoryStruct.comp (groupHomology.π B n) h)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isTopologicalAddGroup : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → AddGroup (R i)] [inst_3 : ∀ (i : ι), AddSubgroupClass (S i) (R i)]
  [∀ (i : ι), IsTopologicalAddGroup (R i)],
  IsTopologicalAddGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Lean.DocString.Types
/-- A user's line break. These are typically ignored when rendering, but don't need to be.
 -/
Lean.Doc.Inline.linebreak : {i : Type u} → String → Lean.Doc.Inline i
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.ret : Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Complex.digamma_one : Complex.digamma 1 = -↑Real.eulerMascheroniConstant
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.faceι.eq_1 : ∀ {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i), SSet.horn.faceι i j hij = SSet.Subcomplex.homOfLE ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
CategoryTheory.to_initial_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {A : C}
  [CategoryTheory.Closed A] [inst_3 : CategoryTheory.Limits.HasInitial C] (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_eq_zero_iff : ∀ {n : Int64}, n.toNatClampNeg = 0 ↔ n ≤ 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
/-- If `f` is monotone on `a..b`, then `f'` is interval integrable on `a..b`.  -/
MonotoneOn.intervalIntegrable_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ}, MonotoneOn f (Set.uIcc a b) → IntervalIntegrable (deriv f) MeasureTheory.volume a b
-- Mathlib.Order.InitialSeg
InitialSeg.lt_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} {b : β} [inst_1 : PartialOrder α] (f : α ≤i β),
  b < f a ↔ ∃ a' < a, f a' = b
-- Mathlib.Geometry.Euclidean.Incenter
/-- The exsphere with signs determined by the given set of indices (for the empty set, this is
the insphere; for a singleton set, this is the exsphere opposite a vertex).  This is only
meaningful if `s.ExcenterExists`; otherwise, it is a sphere of radius zero at some arbitrary
point.  -/
Affine.Simplex.exsphere : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → EuclideanGeometry.Sphere P
-- Mathlib.Data.Set.Lattice
Set.sUnion_singleton : ∀ {α : Type u_1} (s : Set α), ⋃₀ {s} = s
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instMulOneClass : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Monoid R] → [inst_1 : NonUnitalNonAssocSemiring A] → [DistribMulAction R A] → MulOneClass (Unitization R A)
-- Mathlib.Data.Finmap
/-- `all f s` returns `true` iff `f v = true` for all values `v` in `s`.  -/
Finmap.all : {α : Type u} → {β : α → Type v} → ((x : α) → β x → Bool) → Finmap β → Bool
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_symm_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S),
  (AddLocalization.addEquivOfQuotient f).symm (f.mk' x y) = AddLocalization.mk x y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashableMon.hash : Lean.Grind.CommRing.Mon → UInt64
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instSMulMemClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  SMulMemClass (Subalgebra R A) R A
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndep.symm : ∀ {Ω : Type u_1} {m' m₁ m₂ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ → ProbabilityTheory.CondIndep m' m₂ m₁ hm' μ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] (k : α)
  (f : β k → β k), m₁.Equiv m₂ → (m₁.modify k f).Equiv (m₂.modify k f)
-- Init.Data.Array.Lemmas
Array.extract_loop_eq_aux : ∀ {α : Type u_1} {xs ys : Array α} {size start : ℕ},
  Array.extract.loop xs size start ys = ys ++ Array.extract.loop xs size start #[]
-- Init.Data.UInt.Lemmas
UInt32.toNat.eq_1 : ∀ (n : UInt32), n.toNat = n.toBitVec.toNat
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightEq.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r')
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right))),
  CategoryTheory.MorphismProperty.Comma.mapRightEq L r r' h hr =
    CategoryTheory.MorphismProperty.Comma.mapRightEq L r r' h hr
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.insertIfNew! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β},
  l.WF → (Std.DTreeMap.Internal.Impl.insertIfNew! k v l).WF
-- Mathlib.Algebra.Group.Defs
IsCancelAdd.mk : ∀ {G : Type u} [inst : Add G] [toIsLeftCancelAdd : IsLeftCancelAdd G] [toIsRightCancelAdd : IsRightCancelAdd G],
  IsCancelAdd G
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_inter! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  (m₁ m₂ : Std.DTreeMap.Internal.Impl α β),
  m₁.WF →
    m₂.WF →
      (m₁.inter! m₂).toListModel.Perm
        (List.filter (fun p => Std.Internal.List.containsKey p.fst m₂.toListModel) m₁.toListModel)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The image of a family of elements by a morphism of presheaves.  -/
CategoryTheory.Presieve.FamilyOfElements.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} →
          CategoryTheory.Presieve.FamilyOfElements P R → (P ⟶ Q) → CategoryTheory.Presieve.FamilyOfElements Q R
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.closure_prod : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {s : Set G} {t : Set N},
  1 ∈ s → 1 ∈ t → Subgroup.closure (s ×ˢ t) = (Subgroup.closure s).prod (Subgroup.closure t)
-- Mathlib.RingTheory.Derivation.Lie
Derivation.commutator_coe_linear_map : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {D1 D2 : Derivation R A A}, ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
-- Mathlib.Data.Seq.Computation
/-- `get s` returns the result of a terminating computation  -/
Computation.get : {α : Type u} → (s : Computation α) → [h : s.Terminates] → α
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.comp_def : ∀ (Ω : Type w) (S : CategoryTheory.SmallCategoryOfSet Ω) {X Y Z : ↑S.obj} (f : ↑(S.hom X Y)) (g : ↑(S.hom Y Z)),
  CategoryTheory.CategoryStruct.comp f g = S.comp f g
-- Std.Time.Date.Unit.Month
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.days.eq_1 : ∀ (leap : Bool) (month : Std.Time.Month.Ordinal),
  Std.Time.Month.Ordinal.days leap month =
    if ↑month = 2 then if leap = true then 29 else 28
    else
      match Std.Time.Month.Ordinal.monthSizesNonLeap✝ with
      | ⟨months, p⟩ =>
        let index := (Std.Time.Internal.Bounded.LE.sub month 1).toFin Std.Time.Month.Ordinal.days._proof_1✝;
        let idx := Fin.cast ⋯ index;
        months[idx]
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonzero : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {e : Q(«$α»)} → {pα? : Option Q(PartialOrder «$α»)} → Q(«$e» ≠ 0) → Mathlib.Meta.Positivity.Strictness zα e pα?
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- Noether's second isomorphism theorem: given a subgroup `N` of `G` and a
subgroup `H` of the normalizer of `N` in `G`,
defines an isomorphism between `H/(H ∩ N)` and `(H + N)/N`  -/
QuotientAddGroup.quotientInfEquivSumNormalizerQuotient : {G : Type u} →
  [inst : AddGroup G] →
    (H N : AddSubgroup G) →
      (hLE : H ≤ AddSubgroup.normalizer ↑N) → ↥H ⧸ N.addSubgroupOf H ≃+ ↥(H ⊔ N) ⧸ N.addSubgroupOf (H ⊔ N)
-- Mathlib.Data.List.Range
/-- From `l : List ℕ`, construct `l.ranges : List (List ℕ)` such that `l.ranges.map List.length = l`
and `l.ranges.join = range l.sum`
* Example: `[1,2,3].ranges = [[0],[1,2],[3,4,5]]`  -/
List.ranges : List ℕ → List (List ℕ)
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.FiveWheelLikeFree.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (G G_1 : SimpleGraph α),
  G = G_1 → ∀ (r r_1 : ℕ), r = r_1 → ∀ (k k_1 : ℕ), k = k_1 → G.FiveWheelLikeFree r k = G_1.FiveWheelLikeFree r_1 k_1
-- Mathlib.Algebra.Group.TransferInstance
Equiv.Inv.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Inv β], e.Inv = { inv := fun x => e.invFun (e.toFun x)⁻¹ }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_1_comp_cochainsIso₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 1) (groupCohomology.cochainsIso₁ B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).hom (groupCohomology.cochainsMap₁ f φ)
-- Mathlib.Data.Nat.Digits.Div
Nat.dvd_iff_dvd_ofDigits : ∀ (b b' : ℕ) (c : ℤ), ↑b ∣ ↑b' - c → ∀ (n : ℕ), b ∣ n ↔ ↑b ∣ Nat.ofDigits c (b'.digits n)
-- Mathlib.RingTheory.PowerSeries.Order
/-- The `0` power series is the unique power series with infinite order.  -/
PowerSeries.order_eq_top : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ.order = ⊤ ↔ φ = 0
-- Std.Data.ByteSlice
/-- The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the byte slice is
empty.
 -/
Std.Slice.Internal.ByteSliceData.start_le_stop : ∀ (self : Std.Slice.Internal.ByteSliceData), self.start ≤ self.stop
-- Lean.Parser.Types
Lean.Parser.ParserState.pushSyntax : Lean.Parser.ParserState → Lean.Syntax → Lean.Parser.ParserState
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Iic_sdiff_Ioc`. -/
Finset.Iic_diff_Ioc : ∀ {α : Type u_2} {a b : α} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : LocallyFiniteOrderBot α],
  Finset.Iic b \ Finset.Ioc a b = Finset.Iic (min a b)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.comp_neg_X_eq_zero_iff : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, p.comp (-Polynomial.X) = 0 ↔ p = 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldName.sizeOf_spec : ∀ (ref : Lean.Syntax) (name : String) (levels : List Lean.Level) (suffix? : Option Lean.Name) (fullRef : Lean.Syntax),
  sizeOf (Lean.Elab.Term.LVal.fieldName ref name levels suffix? fullRef) =
    1 + sizeOf ref + sizeOf name + sizeOf levels + sizeOf suffix? + sizeOf fullRef
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- The lift of a prefunctor to a groupoid, to a functor from `FreeGroupoid V`  -/
Quiver.FreeGroupoid.lift : {V : Type u} →
  [inst : Quiver V] →
    {V' : Type u'} → [inst_1 : CategoryTheory.Groupoid V'] → V ⥤q V' → CategoryTheory.Functor (Quiver.FreeGroupoid V) V'
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.Quotient.addCommGroup.eq_1 : ∀ {G : Type u_5} [inst : AddCommGroup G] (N : AddSubgroup G),
  QuotientAddGroup.Quotient.addCommGroup N = { toAddGroup := QuotientAddGroup.Quotient.addGroup N, add_comm := ⋯ }
-- Lean.Meta.HaveTelescope
/-- A cached version of the telescope body, instantiated with fvars from each `HaveInfo.decl`.  -/
Lean.Meta.HaveTelescopeInfo.body : Lean.Meta.HaveTelescopeInfo → Lean.Expr
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
_private.Mathlib.NumberTheory.NumberField.Units.DirichletTheorem.0.NumberField.Units.dirichletUnitTheorem.seq.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.RelIso.Basic
RelIso.cast_symm : ∀ {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : r ≍ s),
  (RelIso.cast h₁ h₂).symm = RelIso.cast ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesLimits.createsFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesLimits F] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_stepk_certC : ℤ →
  Lean.Grind.CommRing.Poly →
    ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- `mapCommGrp` is functorial in the left-exact functor.  -/
CategoryTheory.Functor.mapCommGrpFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                CategoryTheory.Functor (C ⥤ₗ D)
                  (CategoryTheory.Functor (CategoryTheory.CommGrp C) (CategoryTheory.CommGrp D))
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv : ∀ {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I)
  {i' j' : J} (h : i' = j'), (CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).inv = CategoryTheory.eqToHom ⋯
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceMod : Lean.Meta.Simp.DSimproc
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_erase_self : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k fallback : α}, (m.erase k).getD k fallback = fallback
-- Mathlib.GroupTheory.Complement
/-- If `H` and `K` are complementary with `K` normal, then `G ⧸ K` is isomorphic to `H`.  -/
Subgroup.IsComplement'.QuotientMulEquiv : {G : Type u_1} → [inst : Group G] → {H K : Subgroup G} → [inst_1 : K.Normal] → H.IsComplement' K → G ⧸ K ≃* ↥H
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.eq_of_eqOn_stop : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S] {f g : F},
  Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Init.Data.Int.Linear
Int.Internal.Linear.le_coeff_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.le_coeff_cert p₁ p₂ k =
    (Int.blt' 0 k).and' ((Int.Internal.Linear.Poly.divCoeffs k p₁).and' (p₂.beq' (Int.Internal.Linear.Poly.div k p₁)))
-- Mathlib.Algebra.Ring.Parity
Odd.neg_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : HasDistribNeg α] {n : ℕ}, Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The formal multilinear series whose `n`-th term is
`(w₁, ..., wₙ) ↦ (-2πI)^n * L v w₁ * ... * L v wₙ • f v`, as a continuous multilinear map in
the space `W [×n]→L[ℝ] E`.

This is designed so that the Fourier transform of `v ↦ fourierPowSMulRight L f v n` is the
`n`-th derivative of the Fourier transform of `f`.
 -/
VectorFourier.fourierPowSMulRight : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      {V : Type u_2} →
        {W : Type u_3} →
          [inst_2 : NormedAddCommGroup V] →
            [inst_3 : NormedSpace ℝ V] →
              [inst_4 : NormedAddCommGroup W] →
                [inst_5 : NormedSpace ℝ W] → (V →L[ℝ] W →L[ℝ] ℝ) → (V → E) → V → FormalMultilinearSeries ℝ W E
-- Mathlib.Tactic.Translate.GuessName
/-- Add the translation `src ↦ tgt` to the `GuessNameExt`.
Both `src` and `tgt` should be capitalized.
This change persists until the end of the current file, but it does not persist through imports.  -/
Mathlib.Tactic.GuessName.GuessNameExt.addTranslation : Mathlib.Tactic.GuessName.GuessNameExt → Lean.Ident → Lean.Ident → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.RingTheory.Multiplicity
finiteMultiplicity_mul_aux : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p : α},
  Prime p → ∀ {a b : α} {n m : ℕ}, ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- The sum over the complement of a finset tends to `0` when the finset grows to
cover the whole space. This does not need a summability assumption, as otherwise all such sums are
zero.  -/
tendsto_tsum_compl_atTop_zero : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  (f : α → G), Filter.Tendsto (fun s => ∑' (a : { x // x ∉ s }), f ↑a) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.ofHom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsAddMonHom f], (CategoryTheory.AddGrp.ofHom f).hom.hom = f
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_of_fmod_eq : ∀ {a b c : ℤ}, a.fmod b = c → b ∣ a - c
-- Lean.Meta.Sym.Arith.Poly
/-- Contains the S-polynomial resulting from superposing two polynomials `p₁` and `p₂`,
along with coefficients and monomials used in their construction.
 -/
Lean.Grind.CommRing.SPolResult : Type
-- Mathlib.Order.Hom.Basic
OrderIso.symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (x : α), e.symm (e x) = x
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.Machine.mk.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (reader : Std.Http.Protocol.H1.Reader dir)
  (writer : Std.Http.Protocol.H1.Writer dir) (config : Std.Http.Protocol.H1.Config)
  (events : Array (Std.Http.Protocol.H1.Event dir)) (error : Option Std.Http.Protocol.H1.Error)
  (instant : Option Std.Time.PlainDateTime) (keepAlive forcedFlush pullBodyStalled : Bool)
  (reader_1 : Std.Http.Protocol.H1.Reader dir) (writer_1 : Std.Http.Protocol.H1.Writer dir)
  (config_1 : Std.Http.Protocol.H1.Config) (events_1 : Array (Std.Http.Protocol.H1.Event dir))
  (error_1 : Option Std.Http.Protocol.H1.Error) (instant_1 : Option Std.Time.PlainDateTime)
  (keepAlive_1 forcedFlush_1 pullBodyStalled_1 : Bool),
  ({ reader := reader, writer := writer, config := config, events := events, error := error, instant := instant,
        keepAlive := keepAlive, forcedFlush := forcedFlush, pullBodyStalled := pullBodyStalled } =
      { reader := reader_1, writer := writer_1, config := config_1, events := events_1, error := error_1,
        instant := instant_1, keepAlive := keepAlive_1, forcedFlush := forcedFlush_1,
        pullBodyStalled := pullBodyStalled_1 }) =
    (reader = reader_1 ∧
      writer = writer_1 ∧
        config = config_1 ∧
          events = events_1 ∧
            error = error_1 ∧
              instant = instant_1 ∧
                keepAlive = keepAlive_1 ∧ forcedFlush = forcedFlush_1 ∧ pullBodyStalled = pullBodyStalled_1)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.exp_arcosh : ∀ {x : ℝ}, 1 ≤ x → Real.exp (Real.arcosh x) = x + √(x ^ 2 - 1)
-- Mathlib.Algebra.NeZero
three_ne_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], 3 ≠ 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.allM_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n]
  [inst_6 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : Std.IterM m β}
  {f : β → n (Option β')} {p : β' → n (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.IterM.filterMapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => p fx
          | none => pure { down := true })
      (Std.IterM.mapM pure it)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Encode `e` as a sequence of keys, computing only the first `Key`.  -/
Lean.Meta.RefinedDiscrTree.initializeLazyEntryWithEtaAux : Lean.Expr → Bool → Lean.MetaM (List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The functor from `Pointed` to `Bipointed` which adds a second point.  -/
pointedToBipointedFst : CategoryTheory.Functor Pointed Bipointed
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_div_mul_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {c : G₀} (a b : G₀), c ≠ 0 → a * c / (b * c) = a / b
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.piQuotientLift.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {N : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N)
  (f f_1 : (i : ι) → Ms i →ₗ[R] N) (e_f : f = f_1) (hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q),
  Submodule.piQuotientLift p q f hf = Submodule.piQuotientLift p q f_1 ⋯
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.of_finite_image : ∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, (f '' s).Finite → Set.InjOn f s → s.Finite
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_comm : ∀ {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β), Graph.banana u v edgeSet = Graph.banana v u edgeSet
-- Lean.Declaration
Lean.OpaqueVal.isUnsafe : Lean.OpaqueVal → Bool