mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- The partial derivative (or directional derivative) in the direction `m : E` as a
continuous linear map on Schwartz space.  -/
SchwartzMap.instLineDeriv : {E : Type u_5} →
  {F : Type u_8} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] → [inst_3 : NormedSpace ℝ E] → LineDeriv E (SchwartzMap E F) (SchwartzMap E F)
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.isKInjective_iff_rightOrthogonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (L : CochainComplex C ℤ),
  L.IsKInjective ↔
    (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
-- Mathlib.Topology.Bases
/-- A set `s` in a topological space is separable if it is contained in the closure of a countable
set `c`. Beware that this definition does not require that `c` is contained in `s` (to express the
latter, use `TopologicalSpace.SeparableSpace s` or
`TopologicalSpace.IsSeparable (univ : Set s)`). In metric spaces, the two definitions are
equivalent, see `TopologicalSpace.IsSeparable.separableSpace`.  -/
TopologicalSpace.IsSeparable : {α : Type u} → [t : TopologicalSpace α] → Set α → Prop
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_sub_le_of_le : ∀ {R : Type u} {n m : ℕ} [inst : Ring R] {p q : Polynomial R},
  p.natDegree ≤ m → q.natDegree ≤ n → (p - q).natDegree ≤ max m n
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instAddSubgroupClass : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G], AddSubgroupClass (ClosedAddSubgroup G) G
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_getKey?_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtDTreeMap α (fun x => Unit) cmp},
  (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁ = t₂
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.isUTF8FirstByte_getUTF8Byte_offset : ∀ {s : String.Slice} {p : s.Pos} {h : p.offset < s.rawEndPos}, (s.getUTF8Byte p.offset h).IsUTF8FirstByte
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisors_iff_left : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {r : M₀}, r ∈ nonZeroDivisors M₀ ↔ ∀ (x : M₀), r * x = 0 → x = 0
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongPrelimit.isSuccPrelimit : ∀ {c : Cardinal.{u_1}}, c.IsStrongPrelimit → Order.IsSuccPrelimit c
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.toHomUnitsMulEquiv_symm_apply : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : CommMonoid M] (f : G →* Mˣ),
  MonoidHom.toHomUnitsMulEquiv.symm f = (Units.coeHom M).comp f
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntryD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a),
  Std.DHashMap.Internal.AssocList.getEntryD a fallback Std.DHashMap.Internal.AssocList.nil = fallback
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_nthRoots : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (n : ℕ) (a : R), (Polynomial.nthRoots n a).card ≤ n
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_one : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M}, (∀ x ∈ s, f x = 1) → ∏ x ∈ s, f x = 1
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_forall_map_eq' : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : Gal(L/F)), IntermediateField.map (↑σ) K = K
-- Init.Data.Int.Gcd
Int.gcd_self_add_left : ∀ (m n : ℤ), (m + n).gcd m = n.gcd m
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instDecidableMem : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → {t : Std.TreeMap.Raw α β cmp} → {a : α} → Decidable (a ∈ t)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.kleinFour_eq_commutator : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → alternatingGroup.kleinFour α = commutator ↥(alternatingGroup α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
eqOn_iteratedDeriv_cotTerm : ∀ (k d : ℕ),
  Set.EqOn (iteratedDeriv k fun z => cotTerm z d)
    (fun z => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k)))
    Complex.integerComplement
-- Init.Data.Array.Lemmas
Array.not_mem_of_not_mem_push : ∀ {α : Type u_1} {a b : α} {xs : Array α}, a ∉ xs.push b → a ∉ xs
-- Batteries.Data.List.Perm
List.Subperm.perm_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ → l₂.length ≤ l₁.length → l₁.Perm l₂
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_apply_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (x : M),
  h.symm (h x) = x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.go.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (k : K) (a : Turing.TM2to1.StAct K Γ σ k) (a_1 : Turing.TM2.Stmt Γ Λ σ),
  sizeOf (Turing.TM2to1.Λ'.go k a a_1) = 1 + sizeOf k + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_proj : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)] (i : ι),
  ↑(ContinuousLinearMap.proj i) = LinearMap.proj i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.instBEqState : BEq Std.Http.Protocol.H1.Writer.State
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.get? (t.min he) = some (t.min he)
-- Aesop.RuleTac.Cases
Aesop.RuleTac.cases : Aesop.CasesTarget → Lean.Meta.TransparencyMode → Bool → Array Aesop.CtorNames → Aesop.RuleTac
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.BuiltinPropagators.mk.inj : ∀ {up down up_1 down_1 : Lean.Meta.Grind.PropagatorMap},
  { up := up, down := down } = { up := up_1, down := down_1 } → up = up_1 ∧ down = down_1
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_iff_submonoid_fg : ∀ {M : Type u_1} [inst : Monoid M] (N : Submonoid M), Monoid.FG ↥N ↔ N.FG
-- Mathlib.Tactic.SetNotationForOrder
/-- Delaborate `x ≤ y` into `x ⊆ y` if the type is tagged with `@[use_set_notation_for_order]`.  -/
Mathlib.Meta.SetNotationForOrder.delabLe : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {fallback : α},
  ∅.maxKeyD fallback = fallback
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have products `a`, `b` respectively, then
the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has
product `a * b`.  -/
HasProd.int_rec : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousMul M] {f g : ℕ → M},
  HasProd f m → HasProd g m' → HasProd (fun t => Int.rec f g t) (m * m')
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapDomain.linearEquiv_symm : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} (f : α ≃ α'), (Finsupp.mapDomain.linearEquiv M R f).symm = Finsupp.mapDomain.linearEquiv M R f.symm
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The unique `RingHom` from `ℤ√d` to a ring `R`, constructed by replacing `√d` with the provided
root. Conversely, this associates to every mapping `ℤ√d →+* R` a value of `√d` in `R`.  -/
Zsqrtd.lift : {R : Type u_1} → [inst : CommRing R] → {d : ℤ} → { r // r * r = ↑d } ≃ (ℤ√d →+* R)
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
ComplexShape.Embedding.stupidTruncFunctor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : e.IsRelIff] (K : HomologicalComplex C c'),
  (e.stupidTruncFunctor C).obj K = K.stupidTrunc e
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
ofAdd_multiset_prod : ∀ {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset M),
  Multiplicative.ofAdd s.sum = (Multiset.map (⇑Multiplicative.ofAdd) s).prod
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filter!_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} {k k' : α} {fallback : β},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filter! f t) k fallback =
        (Option.filter (fun x => f k' x) (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Std.Do.SPred.Laws
Std.Do.SPred.or_elim : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ R) → (Q ⊢ₛ R) → P ∨ Q ⊢ₛ R
-- Aesop.Tree.Data
Aesop.GoalOrigin.copied.inj : ∀ {«from» rep from_1 rep_1 : Aesop.GoalId},
  Aesop.GoalOrigin.copied «from» rep = Aesop.GoalOrigin.copied from_1 rep_1 → «from» = from_1 ∧ rep = rep_1
-- Init.Data.List.Count
List.countP_eq_zero : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, List.countP p l = 0 ↔ ∀ a ∈ l, ¬p a = true
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Pi.sConvexComb_apply : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : ι → Type u_4} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R ((i : ι) → X i))
  (i : ι), Convexity.sConvexComb w i = Convexity.iConvexComb w fun x => x i
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hom_ext' : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D}
  (h : E.IsPointwiseRightKanExtensionAt Y) {T : H} {f g : T ⟶ (CategoryTheory.CostructuredArrow.left E).obj Y},
  (∀ ⦃X : C⦄ (φ : Y ⟶ L.obj X),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map φ)
            ((CategoryTheory.CostructuredArrow.hom E).app X)) =
        CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map φ)
            ((CategoryTheory.CostructuredArrow.hom E).app X))) →
    f = g
-- Mathlib.FieldTheory.PrimitiveElement
Field.primitive_element_inf_aux_exists_c : ∀ {F : Type u_1} [inst : Field F] [Infinite F] {E : Type u_2} [inst_2 : Field E] (ϕ : F →+* E) (α β : E)
  (f g : Polynomial F),
  ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.pow : ∀ {α : Type u_1} {n : Type u_4} [inst : Semiring α] [inst_1 : StarRing α] [inst_2 : Fintype n] [inst_3 : DecidableEq n]
  {A : Matrix n n α}, A.IsHermitian → ∀ (k : ℕ), (A ^ k).IsHermitian
-- Lean.Elab.Coinductive
Lean.Elab.Command.removeFunctorPostfixInCtor : Lean.Name → Lean.Name
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.congrLinearEquiv_trans : ∀ {R : Type u_1} [inst : Semiring R] {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] [inst_3 : AddCommMonoid N₃] [inst_4 : Module R N₁] [inst_5 : Module R N₂]
  [inst_6 : Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃),
  (LinearMap.GeneralLinearGroup.congrLinearEquiv e₁₂).trans (LinearMap.GeneralLinearGroup.congrLinearEquiv e₂₃) =
    LinearMap.GeneralLinearGroup.congrLinearEquiv (e₁₂ ≪≫ₗ e₂₃)
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
MeasureTheory.MemLp.snd : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : X → E × F},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => (f x).2) p μ
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.eq_cuspFunction : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ} (τ : UpperHalfPlane),
  h ≠ 0 →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      UpperHalfPlane.cuspFunction h f (Function.Periodic.qParam h ↑τ) = f τ
-- Aesop.Forward.State
/-- Run an `AddM` action.  -/
Aesop.ClusterState.AddM.run : {α : Type} → Array Lean.MVarId → Array Lean.LMVarId → Aesop.ClusterState.AddM α → Aesop.BaseM (α × Array Aesop.Match)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} (m : ι → MeasurableSpace Ω)
  {_mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.iIndep m κ μ = ProbabilityTheory.Kernel.iIndepSets (fun x => {s | MeasurableSet s}) κ μ
-- Std.Data.TreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
Std.TreeMap.maxEntry : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → t.isEmpty = false → α × β
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel : ∀ {V : Type u} {s : Set (Sym2 V)}, (SimpleGraph.fromEdgeSet s).Reachable = Relation.ReflTransGen (Sym2.ToRel s)
-- Mathlib.Order.Hom.Set
StrictMono.orderIsoOfSurjective_symm_apply_self : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (h_surj : Function.Surjective f) (a : α), (StrictMono.orderIsoOfSurjective f h_mono h_surj).symm (f a) = a
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.eq_maximalIdeal_of_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [inst_2 : IsLocalRing R] (J : Ideal R) [J.IsPrime],
  J = IsLocalRing.maximalIdeal R
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_mem_mem_ne : ∀ {α : Type u} {s : Set α} {x y : α}, x ∈ s → y ∈ s → x ≠ y → s.Nontrivial
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.elems : Lean.Meta.Grind.ParentSet → List Lean.Expr
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_monotone : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M],
  Monotone (Submodule.restrictScalars S)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_eq_one : ∀ {R : Type u} [inst : Semiring R] {a : Polynomial R}, a.toFinsupp = 1 ↔ a = 1
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.Algebra.Group.Defs
npowBinRecAuto.eq_1 : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] (k : ℕ) (m : M), npowBinRecAuto k m = npowBinRec k m
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.forward.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Batteries.Tactic.Alias.AliasInfo.forward n) = 1 + sizeOf n
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKey! k = m.getKey! k
-- Mathlib.Computability.Primrec.Basic
Primrec₂.unpaired : ∀ {α : Type u_1} [inst : Primcodable α] {f : ℕ → ℕ → α}, Primrec (Nat.unpaired f) ↔ Primrec₂ f
-- Mathlib.Order.WithBot
WithBot.le_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithTop αᵒᵈ} {y : WithBot α}, x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
/-- In each positive degree, this lemma decomposes the idempotent endomorphism
`Q q` as a sum of morphisms which are postcompositions with suitable degeneracies.
As `Q q` is the complement projection to `P q`, this implies that in the case of
simplicial abelian groups, any $(n+1)$-simplex $x$ can be decomposed as
$x = x' + \sum (i=0}^{q-1} σ_{n-i}(y_i)$ where $x'$ is in the image of `P q` and
the $y_i$ are in degree $n$.  -/
AlgebraicTopology.DoldKan.decomposition_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n q : ℕ),
  (AlgebraicTopology.DoldKan.Q q).f (n + 1) =
    ∑ i with ↑i < q,
      CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P ↑i).f (n + 1))
        (CategoryTheory.CategoryStruct.comp (X.δ i.rev.succ) (X.σ i.rev))
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_comp_castSucc : ∀ {n : ℕ} {α : Sort u_2} {a : α} {f : Fin n → α}, Fin.snoc f a ∘ Fin.castSucc = f
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
/-- If `M : C` is a monoid object, then `mop M : Cᴹᵒᵖ` too.  -/
MonObj.mopMonObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (M : C) → [CategoryTheory.MonObj M] → CategoryTheory.MonObj { unmop := M }
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
/-- A `1`-cocycle from a cokernel `Q` of `i : A ⟶ B` to a kernel `K` of
`p : X ⟶ Y`. If this is a coboundary, then the square in `CochainComplex C ℤ`
has a lifting, see the lemma `hasLift` below.  -/
CochainComplex.Lifting.cocycle₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B X Y : CochainComplex C ℤ} →
        {t : A ⟶ X} →
          {i : A ⟶ B} →
            {p : X ⟶ Y} →
              {b : B ⟶ Y} →
                (sq : CategoryTheory.CommSq t i p b) →
                  ((n : ℤ) → ⋯.LiftStruct) →
                    {Q : CochainComplex C ℤ} →
                      {π : B ⟶ Q} →
                        {hπ : CategoryTheory.CategoryStruct.comp i π = 0} →
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ) →
                            {K : CochainComplex C ℤ} →
                              {ι : K ⟶ X} →
                                {hι : CategoryTheory.CategoryStruct.comp ι p = 0} →
                                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι) →
                                    CochainComplex.HomComplex.Cocycle Q K 1
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_inr : ∀ (𝕜 : Type u_9) [inst : NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [NontrivialTopology F],
  ‖ContinuousLinearMap.inr 𝕜 E F‖ = 1
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center_prod : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H],
  Subgroup.center (G × H) = (Subgroup.center G).prod (Subgroup.center H)
-- Mathlib.Control.Applicative
instApplicativeAddConstOfZeroOfAdd : {α : Type u_1} → [Zero α] → [Add α] → Applicative (Functor.AddConst α)
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
the partial sums of this power series on the disk of convergence, i.e., `f y`
is the locally uniform limit of `p.partialSum n (y - x)` there.  -/
HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (Metric.eball x r)
-- Lean.Server.FileWorker.SignatureHelp
/-- Cursor is in the position of the argument to a pipe, like `<|` or `$`. Low precedence.
Ensures that `fun <| otherFun <cursor>` yields the signature help of `otherFun`, not `fun`.
 -/
Lean.Server.FileWorker.SignatureHelp.CandidateKind.pipeArg : Lean.Server.FileWorker.SignatureHelp.CandidateKind
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- **Alias** of `AddMonoidAlgebra.coeff_modOf_add_self`. -/
AddMonoidAlgebra.modOf_apply_add_self : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g d : G),
  (x.modOf g).coeff (d + g) = 0
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- An arbitrarily chosen section  -/
GroupExtension.surjInvRightHom : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] → [inst_1 : Group G] → {E : Type u_3} → [inst_2 : Group E] → (S : GroupExtension N E G) → S.Section
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.comp_α_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ) {Z : CochainComplex C ℤ}
  (h : CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.S✝ f n ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α✝ f n) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.closure_nsmul_anti : ∀ {M : Type u_3} [inst : AddMonoid M] {s : Set M} {m n : ℕ},
  m ∣ n → AddSubmonoid.closure (n • s) ≤ AddSubmonoid.closure (m • s)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.step_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {l : List β},
  (l.iterM m).step =
    match l with
    | [] => pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)
    | x :: xs => pure (Std.Shrink.deflate ⟨Std.IterStep.yield (xs.iterM m) x, ⋯⟩)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.lctx : Lean.Meta.Grind.EMatchDiagInfo → Lean.LocalContext