mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_neg : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α), (-a)⁻¹ = -a⁻¹
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoMk.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l l_1 : X.left ≅ Y.left) (e_l : l = l_1)
  (r r_1 : X.right ≅ Y.right) (e_r : r = r_1)
  (h : CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom)),
  CategoryTheory.MorphismProperty.Comma.isoMk l r h = CategoryTheory.MorphismProperty.Comma.isoMk l_1 r_1 ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_lt_iff_contravariant_le : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : LinearOrder N],
  (Covariant M N μ fun x1 x2 => x1 < x2) ↔ Contravariant M N μ fun x1 x2 => x1 ≤ x2
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_lt : ∀ (x : ISize), x.toNatClampNeg < 2 ^ 63
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments of a coercion class (`DFunLike` or `SetLike`)  -/
Simps.findCoercionArgs : Simps.findArgType
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Extract the cone from a bicone.  -/
CategoryTheory.Limits.Bicone.toConeFunctor : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} →
          CategoryTheory.Functor (CategoryTheory.Limits.Bicone F)
            (CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F))
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.Const.toArray.eq_1 : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun x => β),
  Std.DHashMap.Raw.Const.toArray m =
    Std.DHashMap.Raw.fold (fun acc k v => acc.push (k, v)) (Array.emptyWithCapacity m.size) m
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega0_le_omega : ∀ (o : Ordinal.{u_1}), Ordinal.omega0 ≤ Ordinal.omega o
-- Mathlib.Algebra.Group.Units.Equiv
/-- An additive group is isomorphic to its group of additive units  -/
toAddUnits : {G : Type u_5} → [inst : AddGroup G] → G ≃+ AddUnits G
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_Icc : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
  a₁ ∈ Finset.Icc a₂ b₂ → b₁ ∈ Finset.Icc a₂ b₂ → Finset.uIcc a₁ b₁ ⊆ Finset.Icc a₂ b₂
-- Mathlib.Tactic.Simps.Basic
/-- The name used in the generated `simp` lemmas  -/
Simps.ProjectionData.name : Simps.ProjectionData → Lean.Name
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.isKInjective_of_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (L : CochainComplex C ℤ) (d : ℤ) [L.IsStrictlyGE d] [∀ (n : ℤ), CategoryTheory.Injective (L.X n)], L.IsKInjective
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The domain of a morphism.  -/
Mathlib.Tactic.Bicategory.srcExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_succ_right_eq_append_map : ∀ {m n : ℤ}, m ≤ n + 1 → (m...=n + 1).toArray = #[m] ++ Array.map (fun x => x + 1) (m...=n).toArray
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instCoeToLinearMap : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → Coe (LieDerivation R L M) (L →ₗ[R] M)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.Reduced.exists_normalWord_prod_eq : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} (d : Monoid.PushoutI.NormalWord.Transversal φ) {w : Monoid.CoprodI.Word G},
  Monoid.PushoutI.Reduced φ w →
    ∃ w', w'.prod = Monoid.PushoutI.ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.coe_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n), ↑(-z) = -↑z
-- Mathlib.SetTheory.ZFC.Basic
/-- The powerset operation, the collection of subsets of a ZFC set  -/
ZFSet.powerset : ZFSet.{u_1} → ZFSet.{u_1}
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isNormal_preBeth : Order.IsNormal Cardinal.preBeth
-- Init.Data.SInt.Bitwise
Int32.toInt16_or : ∀ (a b : Int32), (a ||| b).toInt16 = a.toInt16 ||| b.toInt16
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S) (r : R) (m : M),
  AddMonoidAlgebra.map f (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single m (f r)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The underlying topological space of a locally ringed space.  -/
AlgebraicGeometry.LocallyRingedSpace.toTopCat : AlgebraicGeometry.LocallyRingedSpace → TopCat
-- Lean.Meta.Tactic.Grind.Cases
/-- We say a free variable is "simple" to be processed by the cases tactic IF:
- It is the latest and consequently there are no forward dependencies, OR
- It is not a proposition.
 -/
_private.Lean.Meta.Tactic.Grind.Cases.0.Lean.Meta.Grind.isSimpleFVar : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Compactness.CountablyCompact
/-- **Alias** of the forward direction of `isCountablyCompact_iff_seq_clusterPt`.

---

A set is countably compact if and only if every sequence eventually in it has a cluster point
in it.  -/
IsCountablyCompact.seq_clusterPt : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  IsCountablyCompact A → ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in Filter.atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a Filter.atTop x
-- Mathlib.Logic.Function.Basic
Function.surjective_to_subsingleton : ∀ {α : Sort u} {β : Sort v} [na : Nonempty α] [Subsingleton β] (f : α → β), Function.Surjective f
-- Mathlib.Combinatorics.Additive.RuzsaCovering
/-- **Ruzsa's covering lemma** for sets. See also `Finset.ruzsa_covering_add`.  -/
Set.ruzsa_covering_add : ∀ {G : Type u_1} [inst : AddGroup G] {K : ℝ} {A B : Set G},
  A.Finite →
    B.Finite →
      B.Nonempty → ↑(Nat.card ↑(A + B)) ≤ K * ↑(Nat.card ↑B) → ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F + (B - B) ∧ F.Finite
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.newHs : Lean.Meta.CaseValuesSubgoal → Array Lean.FVarId
-- Mathlib.LinearAlgebra.Ray
/-- An equivalence between modules implies an equivalence between ray vectors.  -/
RayVector.mapLinearEquiv : {R : Type u_1} →
  [inst : CommSemiring 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] → (M ≃ₗ[R] N) → RayVector R M ≃ RayVector R N
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.prod_mul_tprod_nat_mul' : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousMul M] {f : ℕ → M} {k : ℕ},
  (Multipliable fun n => f (n + k)) → (∏ i ∈ Finset.range k, f i) * ∏' (i : ℕ), f (i + k) = ∏' (i : ℕ), f i
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.φ.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E], ExistsContDiffBumpBase.φ = (Metric.closedBall 0 1).indicator fun x => 1
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.descending_central_series_ge_lower`.

---

Any descending central series for a group is bounded below by the lower central series.  -/
descending_central_series_ge_lower : ∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsDescendingCentralSeries H → ∀ (n : ℕ), ⊤.lowerCentralSeries n ≤ H n
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_cancel_right : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible b], a * ⅟b * b = a
-- Mathlib.Algebra.Lie.Ideal
/-- Transfer the `LieRingModule` instance from the coercion `LieIdeal → LieSubalgebra`.  -/
LieIdeal.lieRingModule : (M : Type w) →
  [inst : AddCommGroup M] →
    {R : Type u_1} →
      {L : Type u_2} →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] → (I : LieIdeal R L) → [LieRingModule L M] → LieRingModule (↥I) M
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.leftUnitor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_le_of_le_le : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] {s t : Set S} {p q : Submodule R M}, s ⊆ t → p ≤ q → s • p ≤ t • q
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.insertAux : {α : Type u_1} →
  {β : Type u_2} →
    [BEq α] → [Hashable α] → Lean.PersistentHashMap.Node α β → USize → USize → α → β → Lean.PersistentHashMap.Node α β
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.backward.dsimp.instances : Lean.Option Bool
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `a = b` and we can evaluate `b`, then we can evaluate `a`.  -/
Mathlib.Meta.NormNum.Result.eq_trans : {u : Lean.Level} →
  {α : Q(Type u)} → {a b : Q(«$α»)} → Q(«$a» = «$b») → Mathlib.Meta.NormNum.Result b → Mathlib.Meta.NormNum.Result a
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State.mk.sizeOf_spec : ∀ (count : ℕ) (results : Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝),
  sizeOf { count := count, results := results } = 1 + sizeOf count + sizeOf results
-- Std.Data.ExtTreeMap.Basic
/-- Removes all mappings of the map for which the given function returns `false`.  -/
Std.ExtTreeMap.filter : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → (α → β → Bool) → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp
-- Mathlib.Data.Sym.Basic
Sym.replicate_succ : ∀ {α : Type u_1} {a : α} {n : ℕ}, Sym.replicate n.succ a = a ::ₛ Sym.replicate n a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) = true ↔
        Std.DTreeMap.Internal.Impl.contains k m₁ = true ∧ Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Batteries.Data.Vector.Lemmas
Vector.toList_scanlM : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : β → α → m β} {as : Vector α n}, Vector.toList <$> Vector.scanlM f init as = List.scanlM f init as.toList
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.instPreorderI₀DirectedAffineCover : {X : AlgebraicGeometry.Scheme} → Preorder X.directedAffineCover.I₀
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.coeff_expand_smul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ),
  p ≠ 0 →
    ∀ (φ : MvPolynomial σ R) (m : σ →₀ ℕ),
      MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) φ) = MvPolynomial.coeff m φ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_of_apply : ∀ {α : Type u} (x : FreeGroup α), (FreeGroup.lift FreeGroup.of) x = x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_ric : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : Std.PRange.Least? α] [inst_3 : LE α] [inst_4 : DecidableLE α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Ric α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible : ∀ {R : Type u} [inst : CommSemiring R],
  PrimeSpectrum.vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}
-- Mathlib.Topology.Constructions.SumProd
continuousAt_prodMap_iff : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Z} {g : Y → W} {x : X} {y : Y},
  ContinuousAt (Prod.map f g) (x, y) ↔ ContinuousAt f x ∧ ContinuousAt g y
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.move.match_1.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (motive : Turing.Dir → Turing.Tape Γ → Sort u_2) (a : Γ)
  (L R : Turing.ListBlank Γ)
  (h_1 : (a : Γ) → (L R : Turing.ListBlank Γ) → motive Turing.Dir.left { head := a, left := L, right := R })
  (h_2 : (a : Γ) → (L R : Turing.ListBlank Γ) → motive Turing.Dir.right { head := a, left := L, right := R }),
  (match Turing.Dir.right, { head := a, left := L, right := R } with
    | Turing.Dir.left, { head := a, left := L, right := R } => h_1 a L R
    | Turing.Dir.right, { head := a, left := L, right := R } => h_2 a L R) =
    h_2 a L R
-- Std.Async.Process
Std.IO.Process.instReprPId : Repr Std.IO.Process.PId
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.le_join_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (m : MeasureTheory.Measure (MeasureTheory.Measure α)) (s : Set α),
  ∫⁻ (μ : MeasureTheory.Measure α), μ s ∂m ≤ m.join s
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongrAddEquiv_apply : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14}
  {M₁' : Type u_15} {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₁']
  [inst_3 : Semiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [inst_12 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_13 : RingHomInvPair σ₂₁ σ₁₂] [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₁ →ₛₗ[σ₁₁'] M₁'), (e₁.arrowCongrAddEquiv e₂) f = (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm
-- Batteries.Data.AssocList
Batteries.AssocList.length_modify : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {l : Batteries.AssocList α β} [inst : BEq α] {a : α},
  (Batteries.AssocList.modify a f l).length = l.length
-- Mathlib.Algebra.DirectSum.Internal
SetLike.homogeneous_zero_submodule : ∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [Zero ι] [inst : Semiring S] [inst_1 : AddCommMonoid R]
  [inst_2 : Module S R] (A : ι → Submodule S R), SetLike.IsHomogeneousElem A 0
-- Mathlib.Tactic.NormNum.Prime
_private.Mathlib.Tactic.NormNum.Prime.0.Mathlib.Meta.NormNum.evalMinFac.aux : (n : Q(ℕ)) →
  (sℕ : Q(AddMonoidWithOne ℕ)) →
    (nn : Q(ℕ)) →
      Q(Mathlib.Meta.NormNum.IsNat «$n» «$nn») →
        ℕ →
          (ek : Q(ℕ)) →
            Q(Mathlib.Meta.NormNum.MinFacHelper «$nn» «$ek») →
              (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat «$n».minFac «$c»)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_zero : ∀ (M₀ : Type u_2) [inst : MonoidWithZero M₀], Ring.inverse 0 = 0
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.intCast_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (n : ℤ), ↑n ∈ S
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.of.injEq : ∀ (η η_1 : Mathlib.Tactic.BicategoryLike.HorizontalComp),
  (Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η = Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η_1) = (η = η_1)
-- Lean.Compiler.NameMangling
Lean.mkModuleInitializationFunctionName : Lean.Name → optParam (Option Lean.PkgId) none → optParam Lean.IRPhases Lean.IRPhases.all → String
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_splitSupport_iff_nonzero : ∀ {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [inst : Zero M] (l : (i : ι) × αs i →₀ M) (i : ι),
  i ∈ l.splitSupport ↔ l.split i ≠ 0
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- We can apply a functor `F : C ⥤ D` to the values of the presheaf in any `PresheafedSpace C`,
giving a functor `PresheafedSpace C ⥤ PresheafedSpace D`  -/
CategoryTheory.Functor.mapPresheaf : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (AlgebraicGeometry.PresheafedSpace C) (AlgebraicGeometry.PresheafedSpace D)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_some_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] (he : t ≠ ∅),
  t.min? = some (t.min he)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.lintegralPowLePowLIntegralFDerivConst_def : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
  (p : ℝ),
  MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p =
    let ι := Fin (Module.finrank ℝ E);
    have this := ⋯;
    let e := ContinuousLinearEquiv.ofFinrankEq this;
    have c := μ.addHaarScalarFactor (MeasureTheory.Measure.map (⇑e.symm) MeasureTheory.volume);
    c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.free_map : ∀ {X Y : CategoryTheory.Quiv} (F : X ⟶ Y),
  CategoryTheory.Cat.free.map F = (CategoryTheory.Cat.freeMap (CategoryTheory.Prefunctor.ofQuivHom F)).toCatHom
-- Init.Data.UInt.Bitwise
instCommutativeUInt64HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.toNegMemClass : ∀ {S : Type u_1} {R : outParam (Type u)} {inst : NonAssocRing R} {inst_1 : SetLike S R} [self : SubringClass S R],
  NegMemClass S R
-- Mathlib.Data.ENat.Lattice
ENat.biSup_add_biSup_le' : ∀ {ι : Sort u_2} {κ : Sort u_3} {f : ι → ℕ∞} {a : ℕ∞} {p : ι → Prop} {q : κ → Prop},
  (∃ i, p i) →
    (∃ j, q j) →
      ∀ {g : κ → ℕ∞},
        (∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a) → (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticTag.unnecessary.sizeOf_spec : sizeOf Lean.Lsp.DiagnosticTag.unnecessary = 1
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
/-- The canonical functor `Karoubi (Karoubi C) ⥤ Karoubi C`  -/
CategoryTheory.Idempotents.KaroubiKaroubi.inverse : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C))
      (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.congr_simp : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  (D D_1 : A → B),
  D = D_1 →
    ∀ [inst_3 : Nonempty A] (f f_1 : AddMonoidAlgebra R A),
      f = f_1 → AddMonoidAlgebra.Monic D f = AddMonoidAlgebra.Monic D_1 f_1
-- Mathlib.Analysis.Calculus.FDeriv.Const
HasStrictFDerivAt.of_notMem_tsupport : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, x ∉ tsupport f → HasStrictFDerivAt f 0 x
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveLimit.measure_univ_unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {μ ν : MeasureTheory.Measure ((i : ι) → α i)},
  MeasureTheory.IsProjectiveLimit μ P → MeasureTheory.IsProjectiveLimit ν P → μ Set.univ = ν Set.univ
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_finrank_eq_one : ∀ {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.center →
    dist p s.center ≠ s.radius → Module.finrank ℝ V = 1 → Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is conjugate linear in the first coordinate.  -/
InnerProductSpace.smul_left : ∀ {𝕜 : Type u_4} {E : Type u_5} {inst : RCLike 𝕜} {inst_1 : SeminormedAddCommGroup E} [self : InnerProductSpace 𝕜 E]
  (x y : E) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y
-- Mathlib.RingTheory.Congruence.Hom
RingCon.ker_comp : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N]
  [inst_2 : NonAssocSemiring P] {f : M →+* N} {g : N →+* P}, RingCon.ker (g.comp f) = (RingCon.ker g).comap f
-- Mathlib.Data.NNReal.Defs
NNReal.instOrderedSub : OrderedSub NNReal
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.contDiffOn_log : ∀ {n : WithTop ℕ∞}, ContDiffOn ℝ n Real.log {0}ᶜ
-- Mathlib.GroupTheory.Transfer
MonoidHom.transfer_eq_pow : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  [inst_2 : H.FiniteIndex] (g : G) (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k),
  ϕ.transfer g = ϕ ⟨g ^ H.index, ⋯⟩
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
coeff_minpolyDiv_mem_adjoin : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S) (i : ℕ),
  (minpolyDiv R x).coeff i ∈ R[x]
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one`.  -/
Right.mul_lt_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b : α},
  a < 1 → b < 1 → a * b < 1