mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Immersion
/-- Let `f : M → N` be a function, and suppose `φ : N → N'` is a `C^n` immersion at `f x`, such
that `φ ∘ f` is `C^n` at `x`. Let `x ∈ t ⊆ M` be contained in the slice chart at `f x`.
Then `f` seen in the slice chart at `φ (f x)` and the preferred chart at `x`
is `C^n` at (the image of) `x` within (the image of) `t`.  -/
_private.Mathlib.Geometry.Manifold.Immersion.0.Manifold.IsImmersionAtOfComplement.aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E''' : Type u_4} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup E'''] [inst_6 : NormedSpace 𝕜 E''']
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] {H : Type u_7} [inst_9 : TopologicalSpace H] {G : Type u_9}
  [inst_10 : TopologicalSpace G] {G' : Type u_10} [inst_11 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H M] {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {N' : Type u_14} [inst_16 : TopologicalSpace N'] [inst_17 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N}
  {φ : N → N'} (h : Manifold.IsImmersionAtOfComplement F J J' n φ (f x)),
  ContMDiffAt I J' n (φ ∘ f) x →
    ∀ {t : Set M},
      t ⊆ f ⁻¹' h.domChart.source →
        x ∈ t →
          ContDiffWithinAt 𝕜 n (↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm)
            (↑(extChartAt I x).symm ⁻¹' t ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Std.Net.Addr
/-- Try to parse `s` as an IPv4 address, returning `none` on failure.
 -/
Std.Net.IPv4Addr.ofString : String → Option Std.Net.IPv4Addr
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_dist_dist_le_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist (dist x z) (dist y z) ≤ dist x y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CancelMonoid α] {s : Finset α} {n : ℕ}, n ≠ 0 → s.card ≤ (s ^ n).card
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.hugeFuel : ℕ
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ G),
  CategoryTheory.Grothendieck.map α =
    { obj := fun X => { base := X.base, fiber := (α.app X.base).toFunctor.obj X.fiber },
      map := fun {X Y} f =>
        { base := f.base,
          fiber :=
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).toNatTrans.app X.fiber)
              ((α.app Y.base).toFunctor.map f.fiber) },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, the result of `secondInter` may be expressed using `lineMap`.  -/
EuclideanGeometry.Sphere.secondInter_eq_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p p' : P),
  s.secondInter p (p' -ᵥ p) =
    (AffineMap.lineMap p p') (-2 * inner ℝ (p' -ᵥ p) (p -ᵥ s.center) / inner ℝ (p' -ᵥ p) (p' -ᵥ p))
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coe_sum`. -/
ProbabilityTheory.Kernel.coe_finsetSum : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_mirror : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.mirror = p
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_def : ∀ {α : Type u_2} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).2 else 0
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.lt_slope_of_hasDerivWithinAt_Iio : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Iio y) y → f' < slope f x y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toList_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ},
  (Std.TreeMap.map f t).toList = List.map (fun p => (p.1, f p.1 p.2)) t.toList
-- Mathlib.Order.Filter.Map
Filter.le_pure_iff : ∀ {α : Type u_1} {f : Filter α} {a : α}, f ≤ pure a ↔ {a} ∈ f
-- Mathlib.RingTheory.Ideal.Operations
Ideal.inf_eq_mul_of_isCoprime : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J → I ⊓ J = I * J
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.toString : Lean.PrettyPrinter.Delaborator.OmissionReason → String
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.congr_arg : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f : A₁ ≃ₐ[R] A₂} {x x' : A₁}, x = x' → f x = f x'
-- Aesop.Forward.Match
/-- Convert forward rule matches to norm rules. Fails if any of the matches is
not a norm rule match.   -/
Aesop.forwardRuleMatchesToNormRules? : Array Aesop.ForwardRuleMatch → Option (Array Aesop.NormRule)
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.doublingGamma_log_convex_Ioi : ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ Real.doublingGamma)
-- Mathlib.CategoryTheory.Localization.FiniteProducts
/-- The functor `limitFunctor L W J` is induced by `lim ⋙ L`.  -/
CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : L.IsLocalization W] →
              (J : Type) →
                [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] →
                  [inst_4 : W.IsStableUnderProductsOfShape J] →
                    [inst_5 : W.ContainsIdentities] →
                      [inst_6 : Finite J] →
                        ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L).comp
                            (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J) ≅
                          CategoryTheory.Limits.lim.comp L
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.bijective_of_isScalarTower' : ∀ {K : Type u_1} {L : Type u_2} {R : Type u_3} [inst : CommRing K] [IsDomain K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : Field R] [inst_5 : Algebra K R] [Module.IsTorsionFree K R] [Algebra.IsAlgebraic K R]
  [inst_8 : Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L), Function.Bijective ⇑f
-- Mathlib.Order.Heyting.Basic
sdiff_le_sdiff_of_sup_le_sup_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ⊔ c ≤ b ⊔ c → a \ c ≤ b \ c
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] {X : I → C} {π : (i : I) → X i ⟶ B}
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks]
  {z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π},
  z₁ = z₂ ↔
    ∀ (ij : I × I),
      (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π
              (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij))
          z₁ =
        (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π
              (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij))
          z₂
-- Lean.Meta.Tactic.Grind.Types
/-- Helper function for executing `x` with a fresh `newFacts` and without modifying
the goal state.
 -/
Lean.Meta.Grind.withoutModifyingState : {α : Type} → Lean.Meta.Grind.GoalM α → Lean.Meta.Grind.GoalM α
-- Mathlib.Data.FunLike.IsApply
IsZeroApply.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two vector spaces are isomorphic if and only if they have the same dimension.  -/
Module.nonempty_linearEquiv_iff_rank_eq : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] [Module.Free R M₁] [StrongRankCondition R],
  Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁
-- Mathlib.Analysis.Asymptotics.Defs
/-- The Landau notation `f =o[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by an arbitrarily small constant
multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` tends to `0` along `l`, modulo division by zero
issues that are avoided by this definition.  -/
Asymptotics.IsLittleO : {α : Type u_18} → {E : Type u_19} → {F : Type u_20} → [Norm E] → [Norm F] → Filter α → (α → E) → (α → F) → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.symm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.VarSet : Type
-- Mathlib.Combinatorics.Hindman
Hindman.FP.below.head' : ∀ {M : Type u_1} [inst : Semigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FP a a_1 → Prop} (a : Stream' M),
  Hindman.FP.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R),
  (CategoryTheory.Limits.Multicoequalizer.multicofork I).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) =
    CategoryTheory.Limits.Multicoequalizer.π I b
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_eq_zero_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  μ.toSphere = 0 ↔ Subsingleton E
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  k ∉ t₂ → Std.ExtDTreeMap.Const.get! (t₁ \ t₂) k = Std.ExtDTreeMap.Const.get! t₁ k
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.mk.injEq : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} (toFun : ι → C(X, ℝ))
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : 0 ≤ toFun) (le_one' : toFun ≤ 1)
  (eventuallyEq_one' : ∀ x ∈ s, ∃ i, ⇑(toFun i) =ᶠ[nhds x] 1) (toFun_1 : ι → C(X, ℝ))
  (locallyFinite'_1 : LocallyFinite fun i => Function.support ⇑(toFun_1 i)) (nonneg'_1 : 0 ≤ toFun_1)
  (le_one'_1 : toFun_1 ≤ 1) (eventuallyEq_one'_1 : ∀ x ∈ s, ∃ i, ⇑(toFun_1 i) =ᶠ[nhds x] 1),
  ({ toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', le_one' := le_one',
        eventuallyEq_one' := eventuallyEq_one' } =
      { toFun := toFun_1, locallyFinite' := locallyFinite'_1, nonneg' := nonneg'_1, le_one' := le_one'_1,
        eventuallyEq_one' := eventuallyEq_one'_1 }) =
    (toFun = toFun_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_toArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toArray.isEmpty = m.isEmpty
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.exists_character_apply_ne_zero_of_ne_zero : ∀ {A : Type uA} [inst : AddCommGroup A] {a : A}, a ≠ 0 → ∃ c, c a ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Composition of morphisms for `WalkingMulticospan`.  -/
CategoryTheory.Limits.WalkingMulticospan.Hom.comp : {J : CategoryTheory.Limits.MulticospanShape} →
  {A B C : CategoryTheory.Limits.WalkingMulticospan J} → A.Hom B → B.Hom C → A.Hom C
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.linearIndependent_aux : ∀ (n k : ℕ), k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `lid_comp_map` that only fires when `g ≠ id`.  -/
CoassocSimps.lid_comp_map_simproc : Lean.Meta.Simp.Simproc
-- Init.Data.List.Monadic
List.flatMapM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : List α}
  {f : α → m (List β)}, List.flatMapM f (wfParam xs) = List.flatMapM f xs.attach.unattach
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.abs : {n : ℕ} → {F : TypeVec.{u} n → Type u_1} → [self : MvQPF F] → {α : TypeVec.{u} n} → ↑(MvQPF.P F) α → F α
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.ω_pow_eq_one : ∀ (p' : ℕ), lucasLehmerResidue (p' + 2) = 0 → LucasLehmer.X.ω ^ 2 ^ (p' + 2) = 1
-- Mathlib.Tactic.HaveI
_private.Mathlib.Tactic.HaveI.0.Mathlib.Tactic.HaveI.termLetIDummy_ : Lean.ParserDescr
-- Mathlib.Data.Fintype.Inv
Function.Embedding.invOfMemRange_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β),
  Function.Surjective f.invOfMemRange
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.instIsCharPOfNatNatOfLawfulOrderLT : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R], Lean.Grind.IsCharP R 0
-- Mathlib.Analysis.Convex.Basic
/-- **Alias** of the forward direction of `convex_iff_ordConnected`. -/
Convex.ordConnected : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜},
  Convex 𝕜 s → s.OrdConnected
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.gateToCNF_eval : ∀ {α : Type u_1} {output lhs rhs : α} {linv rinv : Bool} {assign : α → Bool},
  Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.gateToCNF✝ output lhs rhs linv rinv) =
    (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `addOrder_eq_card_multiples`.  -/
AddRightCancelMonoid.Nat.card_addSubmonoidMultiples : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {a : G}, Nat.card ↥(AddSubmonoid.multiples a) = addOrderOf a
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) {W : Z.Opens}
  (e' : U ≤ (TopologicalSpace.Opens.map g.base).obj W),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e)
      (AlgebraicGeometry.Scheme.Hom.resLE g W U e') =
    AlgebraicGeometry.Scheme.Hom.resLE (CategoryTheory.CategoryStruct.comp f g) W V ⋯
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_le_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atBot → ∀ (c : β), ∀ᶠ (x : α) in l, f x ≤ c
-- Mathlib.Algebra.Group.PUnit
PUnit.zero_eq : 0 = PUnit.unit
-- Mathlib.Order.Heyting.Basic
sdiff_sdiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a \ b) \ a = ⊥
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.instCoalgebraStruct : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid A] →
              [inst_3 : AddCommMonoid B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Module R A] →
                    [inst_6 : Module S A] →
                      [inst_7 : Module R B] →
                        [inst_8 : IsScalarTower R S A] →
                          [CoalgebraStruct R B] → [CoalgebraStruct S A] → CoalgebraStruct S (TensorProduct R A B)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.comp_assoc : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : AddZero M] [inst_1 : AddZero N]
  [inst_2 : AddZero P] [inst_3 : AddZero Q] (f : M →+ N) (g : N →+ P) (h : P →+ Q),
  (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.GroupTheory.Torsion
/-- `g` lies in the `p`-primary component iff `g ^ p ^ k = 1` for some `k`.  -/
CommMonoid.mem_primaryComponent : ∀ {G : Type u_1} [inst : CommMonoid G] {p : ℕ} {g : G}, g ∈ CommMonoid.primaryComponent G p ↔ ∃ k, g ^ p ^ k = 1
-- Std.Data.HashSet.Raw
/-- Removes the element if it exists.  -/
Std.HashSet.Raw.erase : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → α → Std.HashSet.Raw α
-- Mathlib.Data.Countable.Basic
Function.Embedding.countable : ∀ {α : Sort u} {β : Sort v} [Countable β] (f : α ↪ β), Countable α
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.mapToComposableArrows_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ : CategoryTheory.ShortComplex C},
  CategoryTheory.ShortComplex.mapToComposableArrows (CategoryTheory.CategoryStruct.id S₁) =
    CategoryTheory.CategoryStruct.id S₁.toComposableArrows
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.eq_of_ground_subset : ∀ {α : Type u_1} {M N : Matroid α}, N ≤m M → M.E ⊆ N.E → M = N
-- Lean.Server.Completion.CompletionCollectors
/-- Intermediate state while completions are being computed.  -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.State : Type
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_insert : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (x : M) (s : Set M),
  PointedCone.dual p (insert x s) = PointedCone.dual p {x} ⊓ PointedCone.dual p s
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.instToStringFormatError : ToString Mathlib.Linter.FormatError✝
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.className : Lean.Meta.DefaultInstanceEntry → Lean.Name
-- Std.Do.SPred.SVal
Std.Do.SVal.curry_cons : ∀ {α σ : Type u} {σs : List (Type u)} {f : Std.Do.SVal.StateTuple (σ :: σs) → α} {s : σ},
  Std.Do.SVal.curry f s = Std.Do.SVal.curry fun s' => f (s, s')
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.asIdeal_bot : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsDomain R], ⊥.asIdeal = ⊥
-- Mathlib.Data.Finset.Card
Multiset.card_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.toFinset.card = m.dedup.card
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom
        (AlgebraicGeometry.Scheme.Hom.fromNormalization f)) =
    AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iV f)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.galoisConnection_map_functorPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  GaloisConnection (CategoryTheory.Presieve.map F) (CategoryTheory.Presieve.functorPullback F)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_iff_isSome_get? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α}, a ∈ t ↔ (t.get? a).isSome = true
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.coe_addRight : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), ⇑(Equiv.addRight a) = fun x => x + a
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {P : HomotopicalAlgebra.PathObject Y} {f g : X ⟶ Y} (h : P.RightHomotopy f g),
  ∃ P', P'.IsGood ∧ Nonempty (P'.RightHomotopy f g)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (toStarRingEquiv : A ≃⋆+* B)
  (map_smul' : ∀ (r : R) (a : A), toStarRingEquiv.toFun (r • a) = r • toStarRingEquiv.toFun a)
  (toStarRingEquiv_1 : A ≃⋆+* B)
  (map_smul'_1 : ∀ (r : R) (a : A), toStarRingEquiv_1.toFun (r • a) = r • toStarRingEquiv_1.toFun a),
  ({ toStarRingEquiv := toStarRingEquiv, map_smul' := map_smul' } =
      { toStarRingEquiv := toStarRingEquiv_1, map_smul' := map_smul'_1 }) =
    (toStarRingEquiv = toStarRingEquiv_1)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- If the weighted order of a family of `MvPowerSeries` tends to infinity, the collection of all
possible products over `Finset` is summable.  -/
MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top : ∀ {σ : Type u_3} {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {ι : Type u_5}
  {f : ι → MvPowerSeries σ R} [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι] {w : σ → ℕ},
  Filter.Tendsto (fun i => MvPowerSeries.weightedOrder w (f i)) Filter.atTop (nhds ⊤) → Summable fun x => ∏ i ∈ x, f i
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_dualBasis_flip : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate)
  (b : Module.Basis ι K V), B.dualBasis hB (B.flip.dualBasis ⋯ b) = b
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) ⁻¹' Set.Ici b = Set.Ici (b * a)
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_self : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedMul M] (s : Set α)
  (f : α → M), s.mulIndicator f ≤ f
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.add_mul_div_left : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), y ≠ 0 → y ∣ x → (x + y * z) / y = x / y + z
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.multiset_prod_X_sub_C_coeff_card_pred : ∀ {R : Type u} [inst : CommRing R] (t : Multiset R),
  0 < t.card → (Multiset.map (fun x => Polynomial.X - Polynomial.C x) t).prod.coeff (t.card - 1) = -t.sum
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instAddActionOfVAddAssocClass : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} →
          {b : H} →
            {K : Type u_3} →
              [inst_2 : AddMonoid K] →
                [inst_3 : AddAction K H] → [VAddAssocClass K H H] → AddAction K (AddConstMap G H a b)