mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddCommGroupCoeOfAddSubgroupClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddCommGroup (R i)] →
              [∀ (i : ι), AddSubgroupClass (S i) (R i)] →
                AddCommGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Order.Interval.Set.Defs
/-- `Ico a b` is the left-closed right-open interval $[a, b)$.  -/
Set.Ico : {α : Type u_1} → [Preorder α] → α → α → Set α
-- Mathlib.Algebra.Ring.Defs
/-- A `NonUnitalNonAssocSemiring` which `IsMulCommutative` is a `NonUnitalNonAssocCommSemiring`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instNonUnitalNonAssocCommSemiring : {R : Type v} → [inst : NonUnitalNonAssocSemiring R] → [IsMulCommutative R] → NonUnitalNonAssocCommSemiring R
-- Mathlib.Analysis.Normed.Group.Continuity
mem_closure_one_iff_norm : ∀ {E : Type u_4} [inst : SeminormedGroup E] {x : E}, x ∈ closure {1} ↔ ‖x‖ = 0
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.instIsFiniteMeasureSumMeasure : ∀ {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {s : Finset ι} {μ : ι → MeasureTheory.Measure α}
  [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)], MeasureTheory.IsFiniteMeasure (∑ i ∈ s, μ i)
-- Mathlib.Order.CompleteLattice.Basic
le_iSup_of_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι), a ≤ f i → a ≤ iSup f
-- Mathlib.Algebra.CharP.Two
CharTwo.two_zsmul : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] (x : R), 2 • x = 0
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- The submonoid with every element inverted.  -/
Submonoid.inv : {G : Type u_2} → [inst : Group G] → Inv (Submonoid G)
-- Mathlib.Algebra.Category.ModuleCat.Stalk
PresheafOfModules.germ_ringCat_smul : ∀ {X : TopCat} {R : TopCat.Presheaf RingCat X} (M : PresheafOfModules R) (x : ↑X) (U : TopologicalSpace.Opens ↑X)
  (hx : x ∈ U) (r : ↑(R.obj (Opposite.op U))) (m : ↑(M.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) (r • m) =
    (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r •
      (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) m
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The category of R-algebras and their morphisms.  -/
CommAlgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformLeft e x).1.card + (Finset.mulETransformRight e x).1.card = 2 * x.1.card
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.isScalarTower_module : ∀ {R : Type u_6} {A : Type u_7} {M : Type u_8} {M' : Type u_9} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] (S : Submonoid R) [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] [inst_7 : IsLocalization S A] (f : M →ₗ[R] M') [inst_8 : IsLocalizedModule S f],
  IsScalarTower R A M'
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_all_iff_nat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  (∀ (n : ℕ∞), ContDiff 𝕜 (↑n) f) ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f
-- Mathlib.Analysis.Convex.Independent
/-- An indexed family is said to be convex independent if every point only belongs to convex hulls
of sets containing it.  -/
ConvexIndependent : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {ι : Type u_3} → [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommGroup E] → [Module 𝕜 E] → (ι → E) → Prop
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.C.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R],
  MvPolynomial.C = { toFun := ⇑(MvPolynomial.monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.mem_shadow_iterate_iff_exists_card : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
  t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ u, u.card = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.pi.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P),
  QuadraticMap.pi Q = ∑ i, (Q i).comp (LinearMap.proj i)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- the index type of the cells  -/
HomotopicalAlgebra.AttachCells.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} → {X₁ X₂ : C} → {f : X₁ ⟶ X₂} → HomotopicalAlgebra.AttachCells g f → Type w
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ext_iff : ∀ {X Y : CommMonCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_one : bernoulli' 1 = 1 / 2
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_map : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S} {s : Subring R} {y : S},
  y ∈ Subring.map f s ↔ ∃ x ∈ s, f x = y
-- Mathlib.RingTheory.WittVector.Identities
WittVector.coeff_p_zero : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p], (↑p).coeff 0 = 0
-- Mathlib.Data.Set.Card
Set.encard.eq_1 : ∀ {α : Type u_1} (s : Set α), s.encard = ENat.card ↑s
-- Mathlib.Data.Set.MulAntidiagonal
Set.antidiagonal_mono_right : ∀ {α : Type u_1} [inst : Add α] {s t₁ t₂ : Set α} {a : α}, t₁ ⊆ t₂ → s.antidiagonal t₁ a ⊆ s.antidiagonal t₂ a
-- Init.Data.Array.Extract
Array.extract_push_of_le : ∀ {α : Type u_1} {as : Array α} {b : α} {start stop : ℕ},
  stop ≤ as.size → (as.push b).extract start stop = as.extract start stop
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.leadingCoeff_linear : ∀ {R : Type u} {a b : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X + Polynomial.C b).leadingCoeff = a
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.ι₃_desc_assoc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃)
  {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₃
      (CategoryTheory.CategoryStruct.comp (SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) h) =
    CategoryTheory.CategoryStruct.comp f₃ h
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.specOverSpec_over : ∀ {R A : CommRingCat} [inst : Algebra ↑R ↑A],
  AlgebraicGeometry.Spec A ↘ AlgebraicGeometry.Spec R =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_coe : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α} (x : ↑(Set.Ici a)), Set.projIci a ↑x = x
-- Mathlib.Order.Cover
Prod.mk_covBy_mk_iff_left : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {a₁ a₂ : α} {b : β},
  (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
-- Mathlib.Order.InitialSeg
InitialSeg.isLowerSet_range : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : LT α] (f : α ≤i β), IsLowerSet (Set.range ⇑f)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.prod_ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {f g : M × M₂ →L[R] M₃},
  f = g ↔
    f ∘SL ContinuousLinearMap.inl R M M₂ = g ∘SL ContinuousLinearMap.inl R M M₂ ∧
      f ∘SL ContinuousLinearMap.inr R M M₂ = g ∘SL ContinuousLinearMap.inr R M M₂
-- Mathlib.Topology.Category.LightProfinite.Basic
instCategoryLightDiagram' : CategoryTheory.Category.{u_1, u_1} LightDiagram'
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addMonoid.eq_1 : ∀ {M : Type u_4} [inst : AddMonoid M] (c : AddCon M),
  c.addMonoid =
    { toAddSemigroup := c.addSemigroup, toZero := c.zero, zero_add := ⋯, add_zero := ⋯, toNSMul := NSMul.ofSMul,
      nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_finsetProd : ∀ {α : Type u_2} {s : Finset α} {f : α → ℕ},
  (↑s).Pairwise (Function.onFun Nat.Coprime f) →
    ArithmeticFunction.carmichael (s.prod f) = s.lcm (⇑ArithmeticFunction.carmichael ∘ f)
-- Init.Data.Vector.Find
Vector.find?_replicate : ∀ {α : Type} {p : α → Bool} {n : ℕ} {a : α},
  Vector.find? p (Vector.replicate n a) = if n = 0 then none else if p a = true then some a else none
-- Mathlib.Algebra.Star.Subalgebra
/-- Transport a star subalgebra via a star algebra homomorphism.  -/
StarSubalgebra.map : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : StarRing A] →
              [inst_4 : Algebra R A] →
                [inst_5 : StarModule R A] →
                  [inst_6 : Semiring B] →
                    [inst_7 : StarRing B] →
                      [inst_8 : Algebra R B] →
                        [inst_9 : StarModule R B] → (A →⋆ₐ[R] B) → StarSubalgebra R A → StarSubalgebra R B
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.instCocompactMapClass : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  CocompactMapClass (CocompactMap α β) α β
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearEquiv.multilinearMapCongrLeft_symm_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (e : (i : ι) → M₁ i ≃ₗ[R] M₁' i) (a : MultilinearMap R M₁ M₂),
  (LinearEquiv.multilinearMapCongrLeft e).symm a = a.compLinearMap fun x => ↑(e x).symm
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_bot : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂), AffineSubspace.comap f ⊥ = ⊥
-- Mathlib.Order.Antisymmetrization
OrderIso.dualAntisymmetrization_apply : ∀ (α : Type u_1) [inst : Preorder α] (a : α),
  (OrderIso.dualAntisymmetrization α) (OrderDual.toDual (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a)) =
    toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (OrderDual.toDual a)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesKernel.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.PreservesKernel.iso G f = CategoryTheory.Limits.PreservesKernel.iso G f
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.find.eq_1 : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (c : Set (ShrinkingLemma.PartialRefinement u s p)) (ne : c.Nonempty) (i : ι),
  ShrinkingLemma.PartialRefinement.find c ne i = if hi : ∃ v ∈ c, i ∈ v.carrier then hi.choose else ne.some
-- Std.Do.WP.Basic
/-- Soundness lemma for `EStateM.run`.
Useful if you want to prove a property about an expression `x` defined as `EStateM.run prog s` and
you want to use `mvcgen` to reason about `prog`.
 -/
Std.Do.EStateM.of_wp_run_eq : ∀ {ε σ : Type u_1} {s : σ} {α : Type u_1} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α},
  prog.run s = x →
    ∀ (P : EStateM.Result ε σ α → Prop),
      (⊢ₛ
          (Std.Do.wp prog).apply
            (fun a s' => ⌜P (EStateM.Result.ok a s')⌝, fun e s' => ⌜P (EStateM.Result.error e s')⌝, PUnit.unit) s) →
        P x
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The isomorphism `E ⧸ S.rightHom.ker ≃+ G` induced by `S.rightHom`  -/
AddGroupExtension.quotientKerRightHomEquivRight : {N : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup N] →
      [inst_1 : AddGroup G] →
        {E : Type u_3} → [inst_2 : AddGroup E] → (S : AddGroupExtension N E G) → E ⧸ S.rightHom.ker ≃+ G
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
/-- The line graph of a simple graph `G` has its vertex set as the edges of `G`, and two vertices of
the line graph are adjacent if the corresponding edges share a vertex in `G`.
 -/
SimpleGraph.lineGraph : {V : Type u_1} → (G : SimpleGraph V) → SimpleGraph ↑G.edgeSet
-- Mathlib.Data.LawfulXor.Basic
xor_eq_iff_right_eq : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a b c : α), a ^^^ b = c ↔ b = a ^^^ c
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.equivOfIsColimit_apply : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F}
  (hc : CategoryTheory.Functor.CoconeTypes.IsColimit c) (i : C) (x : F i),
  (CategoryTheory.Limits.CofanTypes.equivOfIsColimit hc) ⟨i, x⟩ = c.inj i x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObj_obj_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M] (X : Cᵒᵖ), ↑((CategoryTheory.yonedaMonObj M).obj X) = (Opposite.unop X ⟶ M)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPSummand.eq_1 : ∀ (L : PeriodPair) (x : ℂ) (i : ℕ) (l : ↥L.lattice),
  L.weierstrassPSummand x i l = (↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0
-- Mathlib.GroupTheory.Nilpotent
/-- A group `G` is nilpotent iff there exists an ascending central series which reaches `G` in
finitely many steps.  -/
Subgroup.nilpotent_iff_finite_ascending_central_series : ∀ (G : Type u_1) [inst : Group G], Group.IsNilpotent G ↔ ∃ n H, Subgroup.IsAscendingCentralSeries H ∧ H n = ⊤
-- Mathlib.RingTheory.IsTensorProduct
/-- The isomorphism `S' ≃ S ⊗[R] R` given `Algebra.IsPushout R S R' S'`.  -/
Algebra.IsPushout.equiv : (R : Type u_1) →
  (S : Type v₃) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (R' : Type u_6) →
            (S' : Type u_7) →
              [inst_3 : CommSemiring R'] →
                [inst_4 : CommSemiring S'] →
                  [inst_5 : Algebra R R'] →
                    [inst_6 : Algebra S S'] →
                      [inst_7 : Algebra R' S'] →
                        [inst_8 : Algebra R S'] →
                          [inst_9 : IsScalarTower R R' S'] →
                            [inst_10 : IsScalarTower R S S'] →
                              [h : Algebra.IsPushout R S R' S'] → TensorProduct R S R' ≃ₐ[S] S'
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_single_mul_eq_image : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (f : MonoidAlgebra k G)
  {r : k},
  (∀ (y : k), r * y = 0 ↔ y = 0) →
    ∀ {x : G},
      IsLeftRegular x → (MonoidAlgebra.single x r * f).coeff.support = Finset.image (fun x_1 => x * x_1) f.coeff.support
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_neg : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ), (-A).den = A.den
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_succ : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ),
  LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I =
    ⁅LieAlgebra.derivedSeriesOfIdeal R L k I, LieAlgebra.derivedSeriesOfIdeal R L k I⁆
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v fallback : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l →
              Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k' fallback = v
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.Cofibration.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.cofibrations C f → HomotopicalAlgebra.Cofibration f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_mono : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {f g : ContinuousMapZero (↑(quasispectrum R a)) R}, f ≤ g → (cfcₙHom ha) f ≤ (cfcₙHom ha) g
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single_zero_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (x : AddMonoidAlgebra R M) (r : R)
  (m : M), (AddMonoidAlgebra.single 0 r * x).coeff m = r * x.coeff m
-- Mathlib.Algebra.Module.ULift
ULift.addAction'.eq_1 : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M],
  ULift.addAction' = { toVAdd := ULift.vadd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Std.Data.ExtDTreeMap.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails.  -/
Std.ExtDTreeMap.any : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → ((a : α) → β a → Bool) → Bool
-- Init.Grind.Interactive
/-- `intros` introduces all remaining binders and internalizes them.
Only available in `sym =>` mode.
Use `intros (internalize := false)` or `intros~` to skip internalization.  -/
Lean.Parser.Tactic.Grind.symIntros : Lean.ParserDescr
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Algebra.instCoeDepCoeAlgHomPolynomialAevalSubtypeMemSubalgebraAdjoinSingletonSet : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : Semiring B] →
        [inst_2 : Algebra A B] → (x : B) → (p : Polynomial A) → CoeDep B ((Polynomial.aeval x) p) ↥A[x]
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- Any endomorphism of a fiber functor is a unit.  -/
CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f : CategoryTheory.End F), IsUnit f
-- Mathlib.Order.Filter.Pointwise
Filter.smul_mem_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β},
  s ∈ f → t ∈ g → s • t ∈ f • g
-- Std.Http.Server.Config
/-- The `Server` header value injected into outgoing responses.
`none` suppresses the header entirely.
 -/
Std.Http.Config.serverName : Std.Http.Config → Option Std.Http.Header.Value
-- Mathlib.RingTheory.TensorProduct.Finite
Module.Finite.base_change : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [h : Module.Finite R M], Module.Finite A (TensorProduct R A M)
-- Mathlib.Algebra.Torsor.Basic
Equiv.constVAdd_add : ∀ {G : Type u_1} (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P] (v₁ v₂ : G),
  Equiv.constVAdd P (v₁ + v₂) = Equiv.constVAdd P v₁ * Equiv.constVAdd P v₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a ∈ t.insert k v},
  (t.insert k v).get a h₁ = if h₂ : cmp k a = Ordering.eq then cast ⋯ v else t.get a ⋯
-- Mathlib.Data.Multiset.MapFold
Multiset.map_eq_singleton : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} {b : β}, Multiset.map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix'_toLinearMap₂' : ∀ {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring S₁]
  [inst_4 : Semiring S₂] [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : SMulCommClass S₁ R N₂]
  [inst_8 : SMulCommClass S₂ R N₂] [inst_9 : SMulCommClass S₂ S₁ N₂] [inst_10 : Fintype n] [inst_11 : Fintype m]
  [inst_12 : DecidableEq n] [inst_13 : DecidableEq m] (M : Matrix n m N₂),
  (LinearMap.toMatrix₂' R) ((Matrix.toLinearMap₂' R) M) = M
-- Mathlib.Data.Num.Lemmas
PosNum.cast_pos : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (n : PosNum), 0 < ↑n
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_lt_subst_cert : Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.Data.Matrix.Diagonal
Matrix.ofNat_apply : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] {i j : n} {d : ℕ}
  [inst_2 : d.AtLeastTwo], (OfNat.ofNat d) i j = ↑(if i = j then d else 0)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- The fundamental isCircuit of `e` and `X` has the junk value `{e}` if `e ∈ X`  -/
Matroid.fundCircuit_eq_of_mem : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, e ∈ X → M.fundCircuit e X = {e}
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.Odd.gammaFactor_def : ∀ {N : ℕ} {χ : DirichletCharacter ℂ N}, χ.Odd → ∀ (s : ℂ), χ.gammaFactor s = (s + 1).Gammaℝ
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A nonzero object has nontrivial subobject lattice.  -/
CategoryTheory.Subobject.nontrivial_of_not_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] {X : C},
  ¬CategoryTheory.Limits.IsZero X → Nontrivial (CategoryTheory.Subobject X)