mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.symm_toNatAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S),
  f.toNatAlgEquiv.symm = f.symm.toNatAlgEquiv
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- In the power series expansion of `℘(z) = ∑ aᵢ (z - x)ⁱ` at some `x ∉ L`,
each `aᵢ` can be written as an infinite sum over `l ∈ L`.
This is the summand of this infinite sum with the `l₀`-th term omitted.
See `PeriodPair.coeff_weierstrassPExceptSeries`.  -/
PeriodPair.weierstrassPExceptSummand : (L : PeriodPair) → ℂ → ℂ → ℕ → ↥L.lattice → ℂ
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.zpow` -/
Meromorphic.fun_zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {n : ℤ}, Meromorphic f → Meromorphic fun i => f i ^ n
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- Reinterpret a `NonUnitalSubsemiring` as an `AddSubmonoid`.  -/
NonUnitalSubsemiring.toAddSubmonoid : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → NonUnitalSubsemiring R → AddSubmonoid R
-- Mathlib.Order.Atoms
GaloisInsertion.isAtom_iff' : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α] [IsAtomic α]
  [inst_4 : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u),
  u ⊥ = ⊥ → (∀ (a : α), IsAtom a → u (l a) = a) → ∀ (b : β), IsAtom (u b) ↔ IsAtom b
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.instFinitePresentation : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsFiniteSplit R S], Module.FinitePresentation R S
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_add_neg_eq_addConvolution_neg : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  {ab ∈ A ×ˢ B | ab.1 + -ab.2 = x}.card = A.addConvolution (-B) x
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.uniformEquicontinuous_iff : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {κ₁ : Type u_11}
  {κ₂ : Type u_12} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α},
  (uniformity β).HasBasis p₁ s₁ →
    (uniformity α).HasBasis p₂ s₂ →
      (UniformEquicontinuous F ↔
        ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂)
-- Mathlib.Analysis.Convex.Body
ConvexBody.smul_le_of_le : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V]
  [inst_3 : ContinuousSMul ℝ V] (K : ConvexBody V), 0 ∈ K → ∀ {a b : NNReal}, a ≤ b → a • K ≤ b • K
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₁_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃))
      f₁ =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instCoeSet : {α : Type u_1} → [inst : Preorder α] → Coe (NonemptyInterval α) (Set α)
-- Init.Data.Int.DivMod.Lemmas
Int.lt_of_mul_lt_mul_right : ∀ {a b c : ℤ}, b * a < c * a → 0 ≤ a → b < c
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.param : {α : Type u} → Lean.JsonRpc.Request α → α
-- Mathlib.Topology.Irreducible
IsIrreducible.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set X},
  IsIrreducible t → ∀ {f : Y → X}, Topology.IsOpenEmbedding f → (t ∩ Set.range f).Nonempty → IsIrreducible (f ⁻¹' t)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_le_ofNat : ∀ {o : Ordinal.{u_1}} {n : ℕ} [inst : n.AtLeastTwo], o.card ≤ OfNat.ofNat n ↔ o ≤ OfNat.ofNat n
-- Init.Data.BitVec.Bitblast
BitVec.DivModArgs.mk : {w : ℕ} → BitVec w → BitVec w → BitVec.DivModArgs w
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- A family of sections `sf` is compatible, if the restrictions of `sf i` and `sf j` to `U i ⊓ U j`
agree, for all `i` and `j`
 -/
TopCat.Presheaf.IsCompatible : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type u_3} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X : TopCat} →
              (F : TopCat.Presheaf C X) →
                {ι : Type u_4} →
                  (U : ι → TopologicalSpace.Opens ↑X) →
                    ((i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))) → Prop
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportsParams.mk : Lean.Lsp.LeanModule → Lean.Lsp.LeanModuleHierarchyImportsParams
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_functor_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f : Y ⟶ X),
  ((CategoryTheory.CostructuredArrow.mapIso i).functor.map f).right = CategoryTheory.CategoryStruct.id Y.right
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X), Antitone fun U => Dynamics.netEntropyInfEntourage T F U
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindToInd_apply : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G} (A : Rep.{w, u, v} k ↥S)
  [inst_2 : S.FiniteIndex] (f : ↑(Rep.coind.{u, v, v, w} S.subtype A)),
  A.coindToInd f = ∑ g, g.liftOn (fun g => (Representation.IndV.mk S.subtype A.ρ g) (↑f g)) ⋯
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- When `C` is any category, and `D` is a monoidal category,
the functor category `C ⥤ D` has a natural pointwise monoidal structure,
where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
 -/
CategoryTheory.Monoidal.functorCategoryMonoidalStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.MonoidalCategory D] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Functor C D)
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (F : CategoryTheory.Functor C D) →
          {ι : Type u_3} →
            (c : ComplexShape ι) →
              [inst_2 : CategoryTheory.Preadditive C] →
                [inst_3 : CategoryTheory.Preadditive D] →
                  [inst_4 : CategoryTheory.CategoryWithHomology C] →
                    [inst_5 : CategoryTheory.CategoryWithHomology D] →
                      [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] →
                        [inst_7 : F.Additive] →
                          [inst_8 : F.PreservesHomology] →
                            [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] →
                              CategoryTheory.Localization.Lifting HomologicalComplexUpToQuasiIso.Q
                                (HomologicalComplex.quasiIso C c)
                                ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q)
                                (F.mapHomologicalComplexUpToQuasiIso c)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.constMergeWith : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x_1 => x} {f : α → x → x → x} {h : t₁.Balanced} (a : t₁.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t₁ a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Given two compact sets `K` and `L`, `γ • K ∩ L` is nonempty for finitely many `γ`.  -/
ProperlyDiscontinuousSMul.finite_disjoint_inter_image : ∀ {Γ : Type u_4} {T : Type u_5} {inst : TopologicalSpace T} {inst_1 : SMul Γ T} [self : ProperlyDiscontinuousSMul Γ T]
  {K L : Set T}, IsCompact K → IsCompact L → {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}.Finite
-- Batteries.Data.HashMap.Basic
/-- Converts the map into a list of key-value pairs.
```
open List
(ofList [("one", 1), ("two", 2)]).toList ~ [("one", 1), ("two", 2)]
```
 -/
Batteries.HashMap.toList : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → List (α × β)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instAddZeroClass.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instAddZeroClass = { toZero := AddUnits.instZero, toAdd := AddUnits.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Lean.SubExpr
Lean.SubExpr.Pos.pushLetBody : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedGroup E],
  ULift.seminormedGroup =
    SeminormedGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] [inst_1 : ProbabilityTheory.IsSFiniteKernel η] (a : α),
  ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSectionsOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s t : Set α},
  HasOpenLowerSectionsOn f s → t ⊆ s → HasOpenLowerSectionsOn f t
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.mkHeader : String → Lean.Name → List Lean.Name → Lean.Expr → Lean.DefinitionSafety → Lean.CoreM Lean.MessageData
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousWithinAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {s : Set α} {g : γ → α} {x : γ} {t : Set γ},
  LowerSemicontinuousWithinAt f s (g x) →
    ContinuousWithinAt g t x → Set.MapsTo g t s → LowerSemicontinuousWithinAt (f ∘ g) t x
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composing an alternating map with the same linear map on each argument gives again an
alternating map.  -/
AlternatingMap.compLinearMap : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {M₂ : Type u_10} →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₂] → M [⋀^ι]→ₗ[R] N → (M₂ →ₗ[R] M) → M₂ [⋀^ι]→ₗ[R] N
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulMonC_nc : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulMonC_nc k m p c) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- For a prime ideal `q` in `A⁰_f`, the set `{a | aᵢᵐ/fⁱ ∈ q}` as an ideal.
 -/
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace →
                        Ideal A
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.opFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b),
  (Bicategory.Opposite.opFunctor a b).obj f = f.op
-- Mathlib.Analysis.Normed.Module.RCLike.Real
frontier_sphere : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ},
  r ≠ 0 → frontier (Metric.sphere x r) = Metric.sphere x r
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The whole group `G` is normal.  -/
Subgroup.normal_top : ∀ {G : Type u_1} [inst : Group G], ⊤.Normal
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.comp_injective : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [NoMaxOrder β] [Nonempty β]
  {u : ℕ → α}, CauchySeq u → ∀ {f : β → ℕ}, Function.Injective f → CauchySeq (u ∘ f)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- See also `RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic`.  -/
RootPairing.rootForm_restrict_nondegenerate_of_ordered : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N), LinearMap.Nondegenerate (P.RootForm.restrict (P.rootSpan R))
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a finite power series on a ball, then so does its derivative.  -/
HasFiniteFPowerSeriesOnBall.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E},
  HasFiniteFPowerSeriesOnBall f p x (n + 1) r → HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r
-- Mathlib.Data.Sym.Basic
Sym.count_coe_fill_self_of_notMem : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] {a : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)},
  a ∉ s → Multiset.count a ↑(Sym.fill a i s) = ↑i
-- Mathlib.Data.List.DropRight
List.rtakeWhile_suffix : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rtakeWhile p l <:+ l
-- Mathlib.RingTheory.Extension.Basic
/-- An `R`-extension `P → S` gives an `R`-extension `Pₘ → Sₘ`.
Note that this is different from `baseChange` as the base does not change.
 -/
Algebra.Extension.localization : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Submonoid S) →
            {S' : Type u_1} →
              [inst_3 : CommRing S'] →
                [inst_4 : Algebra S S'] →
                  [IsLocalization M S'] →
                    [inst_6 : Algebra R S'] → [IsScalarTower R S S'] → Algebra.Extension R S → Algebra.Extension R S'
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesLimitIso_inv_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F] (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.π F j)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp G) j) h
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_3.splitter : (n : ℕ) →
  (P : Fin (n + 1) → Prop) →
    (inst : DecidablePred P) →
      (motive : (k : ℕ) → (k < Fin.countP fun x => decide (P x)) → Sort u_1) →
        (k : ℕ) →
          (hk : k < Fin.countP fun x => decide (P x)) →
            ((hk : 0 < Fin.countP fun x => decide (P x)) → motive 0 hk) →
              ((k : ℕ) → (hk : k + 1 < Fin.countP fun x => decide (P x)) → motive k.succ hk) → motive k hk
-- Lean.Meta.Tactic.Grind.Core
/-- Returns `true` if the parent is relevant for congruence closure.
 -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.isCongrRelevant : Lean.Expr → Bool
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_bot : ∀ {V : Type u_1}, (SimpleGraph.emptyGraph V).vertexCoverNum = 0
-- Mathlib.Data.Multiset.MapFold
Multiset.foldl_induction' : ∀ {α : Type u_1} {β : Type v} (f : β → α → β) [inst : RightCommutative f] (x : β) (q : α → Prop) (p : β → Prop)
  (s : Multiset α), (∀ (a : α) (b : β), q a → p b → p (f b a)) → p x → (∀ a ∈ s, q a) → p (Multiset.foldl f x s)
-- Mathlib.LinearAlgebra.Projection
Submodule.range_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), (p.projection q hpq).range = p
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Adjunction between two 1-morphisms.  -/
CategoryTheory.Bicategory.«term_⊣_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- If the quotient by a subgroup gives a singleton then the subgroup is the whole group.  -/
QuotientGroup.subgroup_eq_top_of_subsingleton : ∀ {G : Type u} [inst : Group G] (H : Subgroup G), Subsingleton (G ⧸ H) → H = ⊤
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- The set of all complex embeddings of `L` that lie over `ψ` and are mixed.  -/
NumberField.ComplexEmbedding.mixedEmbeddingsOver : {K : Type u_3} → (L : Type u_4) → [inst : Field K] → [inst_1 : Field L] → (K →+* ℂ) → [Algebra K L] → Set (L →+* ℂ)
-- Batteries.Data.Char.Basic
_private.Batteries.Data.Char.Basic.0.Char.of_any_eq_false_aux : ∀ {p : Char → Bool}, Char.any p = false → ∀ (n : ℕ) (hn : n.isValidChar), p (Char.ofNatAux n hn) = false
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_alter_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = false → (k' ∈ Std.DHashMap.Const.alter m k f ↔ k' ∈ m)
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.instPowWithConvNat : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] → [inst_3 : Bialgebra R C] → [inst_4 : Algebra R A] → Pow (WithConv (C →ₐ[R] A)) ℕ
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying morphism of the inverse component of the left unitor isomorphism.  -/
Bimod.LeftUnitorBimod.inv : {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) → P.X ⟶ Bimod.TensorBimod.X (Bimod.regular R) P
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁` is not a subsequence of `s₂`  -/
Lean.Grind.AC.SubseqResult.false : Lean.Grind.AC.SubseqResult
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.collect : Lean.Level → Lean.CollectLevelMVars.Visitor
-- Init.Data.List.Monadic
List.mapM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : List α} {f : α → m β},
  List.mapM f (wfParam xs) = List.mapM f xs.attach.unattach
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x + a) ⁻¹' Set.Ioc b c = Set.Ioc (b - a) (c - a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (t.erase k).maxKey he = t.maxKey ⋯ ↔ ¬cmp k (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Topology.Perfect
Perfect.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α}, IsClosed C → Preperfect C → Perfect C
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalAevalEquiv_apply_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (xy : A × A)
  (x : Polynomial (Polynomial R)),
  ((Polynomial.aevalAevalEquiv R A) xy) x = Polynomial.eval xy.1 ((Polynomial.aeval (Polynomial.C xy.2)) x)
-- Lean.Server.Requests
Lean.Server.RequestM.bindTaskCostly : {α : Type u_1} →
  {β : Type} →
    Lean.Server.ServerTask α →
      (α → Lean.Server.RequestM (Lean.Server.RequestTask β)) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Lean.Compiler.Specialize
Lean.Compiler.SpecializeAttributeKind.noConfusionType : Sort v✝ → Lean.Compiler.SpecializeAttributeKind → Lean.Compiler.SpecializeAttributeKind → Sort v✝
-- Init.Data.Int.Order
Int.sub_lt_sub_of_le_of_lt : ∀ {a b c d : ℤ}, a ≤ b → c < d → a - d < b - c
-- Mathlib.Data.Multiset.Filter
Multiset.filter_eq_nil : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α}, Multiset.filter p s = 0 ↔ ∀ a ∈ s, ¬p a
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.mk : {m : Type w → Type w'} → {β : Type w} → (α : Type w) → Std.Iterator α m β → Std.IterM m β → Std.BundledIterM m β
-- Mathlib.Analysis.Complex.IntegerCompl
/-- **Alias** of `Complex.mem_integerComplement_iff`. -/
Complex.integerComplement.mem_iff : ∀ {x : ℂ}, x ∈ Complex.integerComplement ↔ ¬∃ n, ↑n = x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.adj_sub' : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (u v : ↑G'.verts), G'.Adj ↑u ↑v → G.Adj ↑u ↑v
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).hom =
    CategoryTheory.CategoryStruct.comp (F.map (e.unit.app j))
      (CategoryTheory.CategoryStruct.comp (w.inv.app ((e.functor.comp e.inverse).obj j))
        (CategoryTheory.Limits.colimit.ι G (e.functor.obj ((e.functor.comp e.inverse).obj j))))
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.ofIdComp_right_as : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)),
  t.ofIdComp.right.as = PUnit.unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_union_of_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors_eq_singleton_one_iff_prime : ∀ {n : ℕ}, n.properDivisors = {1} ↔ Nat.Prime n
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range_eq_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), f.range = Subgroup.map f ⊤