mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ne_single_iff : ∀ {n : ℕ} (hn : 0 < n) {c : Composition n}, c ≠ Composition.single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.subset_smul_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A B : Set β} {a : α}, A ⊆ a • B ↔ a⁻¹ • A ⊆ B
-- Lean.Parser.Types
Lean.Parser.initCacheForInput : String → Lean.Parser.ParserCache
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
/-- Let `K` be a finite field of cardinality `p ^ f` and let `P` be an irreducible factor of the
`n`-th cyclotomic polynomial over `K`, where `p` and `n` are coprime. This result computes the
number of distinct irreducible factors of `cyclotomic n K`.  -/
Polynomial.normalizedFactors_cyclotomic_card : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] [inst_2 : DecidableEq K],
      (UniqueFactorizationMonoid.normalizedFactors (Polynomial.cyclotomic n K)).toFinset.card =
        n.totient / orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsFiniteKernel.isFiniteMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsFiniteKernel κ] (a : α), MeasureTheory.IsFiniteMeasure (κ a)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.State.mk.injEq : ∀ {α : Type} (producers : Std.Queue (IO.Promise Bool)) (waiters : Std.Queue (Std.Broadcast.Consumer✝ α))
  (capacity : { x // 0 < x }) (size : ℕ) (buffer : Vector (IO.Ref (Std.Slot✝ α)) ↑capacity) (write read : Fin ↑capacity)
  (receivers : Std.TreeMap ℕ ℕ compare) (nextId : ℕ) (closed : Bool) (pos : ℕ)
  (producers_1 : Std.Queue (IO.Promise Bool)) (waiters_1 : Std.Queue (Std.Broadcast.Consumer✝ α))
  (capacity_1 : { x // 0 < x }) (size_1 : ℕ) (buffer_1 : Vector (IO.Ref (Std.Slot✝ α)) ↑capacity_1)
  (write_1 read_1 : Fin ↑capacity_1) (receivers_1 : Std.TreeMap ℕ ℕ compare) (nextId_1 : ℕ) (closed_1 : Bool)
  (pos_1 : ℕ),
  ({ producers := producers, waiters := waiters, capacity := capacity, size := size, buffer := buffer, write := write,
        read := read, receivers := receivers, nextId := nextId, closed := closed, pos := pos } =
      { producers := producers_1, waiters := waiters_1, capacity := capacity_1, size := size_1, buffer := buffer_1,
        write := write_1, read := read_1, receivers := receivers_1, nextId := nextId_1, closed := closed_1,
        pos := pos_1 }) =
    (producers = producers_1 ∧
      waiters = waiters_1 ∧
        capacity = capacity_1 ∧
          size = size_1 ∧
            buffer ≍ buffer_1 ∧
              write ≍ write_1 ∧
                read ≍ read_1 ∧ receivers = receivers_1 ∧ nextId = nextId_1 ∧ closed = closed_1 ∧ pos = pos_1)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_inv : ∀ {u : ℕ → ENNReal}, ExpGrowth.expGrowthInf u⁻¹ = -ExpGrowth.expGrowthSup u
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given a functor `F : D ⥤ C`, this is a predicate on objects `X : C` corresponding
to the domain of definition of the (partial) left adjoint of `F`.  -/
CategoryTheory.Functor.leftAdjointObjIsDefined : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D C → CategoryTheory.ObjectProperty C
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_iSup_directed_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) → ProbabilityTheory.Indep (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) μ
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion `U i ⟶ iSup U` as a morphism in the category of open sets.
 -/
TopologicalSpace.Opens.leSupr : {X : TopCat} → {ι : Type u_1} → (U : ι → TopologicalSpace.Opens ↑X) → (i : ι) → U i ⟶ iSup U
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.sub : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)]
  {f g : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s p f →
    TemperedDistribution.MemSobolev s p g → TemperedDistribution.MemSobolev s p (f - g)
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.expectedType? : Lean.Elab.Term.FunBinders.State → Option Lean.Expr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β}, k' ∈ m.modify k f ↔ k' ∈ m
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_closure : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {x : G},
  x ∈ AddSubgroup.closure k ↔ ∀ (K : AddSubgroup G), k ⊆ ↑K → x ∈ K
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_biUnion_partition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
  (∀ J ∈ π, (πi J).IsPartition) → (π.biUnion πi).iUnion = π.iUnion
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasStrictDerivAt.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
  HasStrictDerivAt c c' x →
    HasStrictDerivAt d d' x → d x ≠ 0 → HasStrictDerivAt (c / d) ((c' * d x - c x * d') / d x ^ 2) x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_mapM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_10 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [inst_12 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_14 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.IterM.mapM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      g __do_lift acc
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.IsHamiltonian.mono : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α] {H : SimpleGraph α},
  G ≤ H → G.IsHamiltonian → H.IsHamiltonian
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- Reindex a product over `Nat.Primes` as a product over `ℕ`, extending `f` by `1`.  -/
Nat.Primes.tprod_eq_tprod_ite : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M),
  ∏' (p : Nat.Primes), f ↑p = ∏' (n : ℕ), if Nat.Prime n then f n else 1
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.surjective_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.Surjective
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.comp_tendsto : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {ι' : Type u_4} {l' : Filter ι'} {φ : ι' → ι},
  IsAddFoelner G μ l F → Filter.Tendsto φ l' l → IsAddFoelner G μ l' (F ∘ φ)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.of_prefixFunction_eq : ∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    needlePos ≠ 0 →
      ∀ {k : ℕ} {hki : needlePos.byteIdx - 1 < pat.copy.toByteArray.size},
        String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat.copy.toByteArray (needlePos.byteIdx - 1)
              hki =
            k →
          0 < k → String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s { byteIdx := k } stackPos
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_preimage_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : ℝ},
  r ≠ 0 → ∀ (s : Set E), μ ((fun x => r • x) ⁻¹' s) = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| * μ s
-- Lean.Data.Lsp.Basic
Lean.Lsp.Command.mk.inj : ∀ {title command : String} {arguments? : Option (Array Lean.Json)} {title_1 command_1 : String}
  {arguments?_1 : Option (Array Lean.Json)},
  { title := title, command := command, arguments? := arguments? } =
      { title := title_1, command := command_1, arguments? := arguments?_1 } →
    title = title_1 ∧ command = command_1 ∧ arguments? = arguments?_1
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
/-- The free monoid on `α` is isomorphic to the free semigroup on `α` with a `1` added.
 -/
FreeMonoid.equivWithOneFreeSemigroup : {α : Type u_1} → FreeMonoid α ≃* WithOne (FreeSemigroup α)
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- Being integrally closed is preserved under injective algebra homomorphisms.  -/
AlgHom.isIntegrallyClosedIn : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Injective ⇑f → IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.mk.injEq : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (C U : Set X) (P_C_U : P C U)
  (closed_C : IsClosed C) (open_U : IsOpen U) (subset : C ⊆ U)
  (hP :
    ∀ {c u : Set X},
      IsClosed c → P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u)
  (C_1 U_1 : Set X) (P_C_U_1 : P C_1 U_1) (closed_C_1 : IsClosed C_1) (open_U_1 : IsOpen U_1) (subset_1 : C_1 ⊆ U_1)
  (hP_1 :
    ∀ {c u : Set X},
      IsClosed c → P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u),
  ({ C := C, U := U, P_C_U := P_C_U, closed_C := closed_C, open_U := open_U, subset := subset, hP := hP } =
      { C := C_1, U := U_1, P_C_U := P_C_U_1, closed_C := closed_C_1, open_U := open_U_1, subset := subset_1,
        hP := hP_1 }) =
    (C = C_1 ∧ U = U_1)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddHom.pi_apply`. -/
Pi.addHom_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {γ : Type w} [inst_1 : Add γ] (g : (i : I) → γ →ₙ+ f i)
  (x : γ) (i : I), (AddHom.pi g) x i = (g i) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m)).Equiv ↑m ↔
      ∀ (a : α) (h : m.contains a = true), f (m.getKey a h) = true)
-- Init.Control.ExceptCps
ExceptCpsT.run_pure : ∀ {m : Type u_1 → Type u_2} {ε α : Type u_1} {x : α} [inst : Monad m], (pure x).run = pure (Except.ok x)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.transpose_nonsing_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  A⁻¹.transpose = A.transpose⁻¹
-- Mathlib.CategoryTheory.Subfunctor.Subobject
/-- The equivalence of categories `Subfunctor F ≌ MonoOver F`.  -/
CategoryTheory.Subfunctor.equivalenceMonoOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) → CategoryTheory.Subfunctor F ≌ CategoryTheory.MonoOver F
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow.congr_simp : ∀ {p p_1 : ℕ} (e_p : p = p_1) {k k_1 : ℕ} (e_k : k = k_1) {K : Type u} [inst : Field K] {ζ : K}
  [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K] [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K]
  (hζ : IsPrimitiveRoot ζ (p ^ k)), hζ.adjoinEquivRingOfIntegersOfPrimePow = ⋯.adjoinEquivRingOfIntegersOfPrimePow
-- Init.Data.Nat.Lemmas
Nat.sub_lt_sub_iff_right : ∀ {a b c : ℕ}, c ≤ a → (a - c < b - c ↔ a < b)
-- Mathlib.Data.Seq.Computation
Computation.destruct_pure : ∀ {α : Type u} (a : α), (Computation.pure a).destruct = Sum.inl a
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_four : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS b c d 4 = d
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.unop2_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  (CategoryTheory.CategoryStruct.comp η θ).unop2 = CategoryTheory.CategoryStruct.comp η.unop2 θ.unop2
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_dite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι)
  (b : (x : ι) → x = a → M), (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1
-- Mathlib.LinearAlgebra.InvariantBasisNumber
eq_of_fin_equiv : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R] {n m : ℕ} (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The forward map of a homeomorphism is a continuous function.  -/
ContinuousAlgEquiv.continuous_toFun : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (self : A ≃A[R] B), Continuous self.toFun
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↑X.toTopCat) (hxx' : x = x')
  {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ⋯) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g x') h)
-- Qq.ForLean.Do
_private.Qq.ForLean.Do.0.Lean.Elab.Term.extractBind.extract? : (Lean.Expr → Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult)) →
  Lean.Expr → Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isSemisimpleRing_iff_jacobson : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing R], IsSemisimpleRing R ↔ Ring.jacobson R = ⊥
-- Mathlib.Topology.Sets.CompactOpenCovered
/-- A set `U` is compact-open covered by the family `fᵢ : X i → S`, if
`U` is the finite union of images of compact open sets in the `X i`.  -/
IsCompactOpenCovered : {S : Type u_1} →
  {ι : Type u_2} → {X : ι → Type u_3} → ((i : ι) → X i → S) → [(i : ι) → TopologicalSpace (X i)] → Set S → Prop
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.mk_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) (i : ι),
  (Module.Basis.mk hli hsp) i = v i
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.const : ∀ {α : Type u_1} {m : MeasurableSpace α} (p : Prop), MeasurableSet {_a | p}
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_ofNat : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : ℕ} [inst_3 : n.AtLeastTwo], (OfNat.ofNat n).IsPositive
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyAt.congr_simp : ∀ {s : String.Slice} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos),
  String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h = String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos_1 ⋯
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.enoughInjectives_of_enoughProjectives_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughProjectives Cᵒᵖ],
  CategoryTheory.EnoughInjectives C
-- Lean.Elab.MutualInductive
Lean.Elab.Command.checkValidCtorModifier : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Elab.Modifiers → m Unit
-- Mathlib.Data.ZMod.Defs
ZMod.inhabited : (n : ℕ) → Inhabited (ZMod n)
-- Mathlib.Analysis.Calculus.Implicit
/-- **Alias** of `ImplicitFunctionData.leftFun_implicitFunction`. -/
ImplicitFunctionData.left_map_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (p : F × G) in nhds (φ.prodFun φ.pt), φ.leftFun (φ.implicitFunction p.1 p.2) = p.1
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_one_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Zero G], (AddMonoidAlgebra.coeff 1).support ⊆ 0
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms.0.SimplexCategoryGenRel.simplicialInsert.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (b : ℕ) → (l : List ℕ) → motive (b :: l)),
  (match [] with
    | [] => h_1 ()
    | b :: l => h_2 b l) =
    h_1 ()
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache : {w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr.Cache aig → Std.Tactic.BVDecide.BVExpr.Return aig w
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationPullback f g)
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g) =
    AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.Limits.pullback.snd f g)
-- Init.Core
/-- If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
 -/
PSum.inhabitedLeft : {α : Sort u_1} → {β : Sort u_2} → [Inhabited α] → Inhabited (α ⊕' β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t ↔ (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X},
  CategoryTheory.IsKernelPair f a b → ∀ [CategoryTheory.Mono f], CategoryTheory.IsIso a
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.instPUnit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)], Topology.IsGeneratedBy X PUnit.{v + 1}
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.age.is_equiv_invariant : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] (N P : CategoryTheory.Bundled L.Structure),
  Nonempty (L.Equiv ↑N ↑P) → (N ∈ L.age M ↔ P ∈ L.age M)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_append : ∀ {m n : ℕ}, m + 1 < n → (m<...n).toList = (m<...n - 1).toList ++ [n - 1]
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- The composition of étale morphisms is étale.  -/
AlgebraicGeometry.Etale.etale_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [AlgebraicGeometry.Etale f]
  [AlgebraicGeometry.Etale g], AlgebraicGeometry.Etale (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.comp.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] {X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y) (g : Y.Hom Z),
  sizeOf (f.comp g) = 1 + sizeOf X + sizeOf Y + sizeOf Z + sizeOf f + sizeOf g
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgEquiv.ofInjective_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (x : A),
  ↑((AlgEquiv.ofInjective f hf) x) = f x
-- Mathlib.Data.Nat.Nth
Nat.nth_mem : ∀ {p : ℕ → Prop} (n : ℕ), (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → p (Nat.nth p n)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.projectRightAssign_property : ∀ {assign : ℕ → Bool} {x : ℕ}, Std.Sat.AIG.toCNF.projectRightAssign✝ assign x = assign x
-- Mathlib.Data.Set.Insert
Set.inter_singleton_nonempty : ∀ {α : Type u_1} {s : Set α} {a : α}, (s ∩ {a}).Nonempty ↔ a ∈ s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β k}, a ∈ m.insert k v → (k == a) = false → a ∈ m
-- Mathlib.Analysis.Seminorm
/-- Balls at the origin are absorbent.  -/
absorbent_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, 0 < r → Absorbent 𝕜 (Metric.ball 0 r)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A reversed telescoping product along `{0, ..., n - 1}` of a commutative-group-valued function
reduces to the ratio of the first and last factors.  -/
Finset.prod_range_div' : ∀ {G : Type u_3} [inst : CommGroup G] (f : ℕ → G) (n : ℕ), ∏ i ∈ Finset.range n, f i / f (i + 1) = f 0 / f n
-- Mathlib.ModelTheory.Fraisse
/-- Sufficient conditions for a class to be the age of a countably-generated structure.  -/
FirstOrder.Language.exists_cg_is_age_of : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
  K.Nonempty →
    (Quotient.mk' '' K).Countable →
      (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) →
        FirstOrder.Language.Hereditary K →
          FirstOrder.Language.JointEmbedding K → ∃ M, FirstOrder.Language.Structure.CG L ↑M ∧ L.age ↑M = K
-- Mathlib.Order.SuccPred.Limit
SuccOrder.limitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a)
  (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a),
  SuccOrder.limitRecOn b isMin succ isSuccLimit =
    SuccOrder.prelimitRecOn b succ fun a ha IH => if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH
-- Init.Data.Array.Lemmas
Array.extract.eq_1 : ∀ {α : Type u_1} (as : Array α) (start stop : ℕ),
  as.extract start stop =
    Array.extract.loop as ((min stop as.size).sub start) start (Array.emptyWithCapacity ((min stop as.size).sub start))