mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_mono : ∀ {α : Type u} [inst : Semiring α] {s t : Set α}, s ⊆ t → Ideal.span s ≤ Ideal.span t
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_injective : ∀ {L : Type u_2} {R : Type u_3} [inst : Field L] [inst_1 : CommRing R] [Nontrivial R] (φ : Polynomial R →+* L)
  (hφ : Function.Injective ⇑φ)
  (hφ' : optParam (nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) ⋯),
  Function.Injective ⇑(RatFunc.liftRingHom φ hφ')
-- Mathlib.Data.Set.Operations
/-- The graph of a function `f : α → β` on a set `s`.  -/
Set.graphOn : {α : Type u} → {β : Type v} → (α → β) → Set α → Set (α × β)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.eventually_constant_sum : ∀ {M : Type u_4} [inst : AddCommMonoid M] {u : ℕ → M} {N : ℕ},
  (∀ n ≥ N, u n = 0) → ∀ {n : ℕ}, N ≤ n → ∑ k ∈ Finset.range n, u k = ∑ k ∈ Finset.range N, u k
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The subgroup of Dirichlet characters of level `n` whose primitive character sends the prime `p`
to `1`. See `mem_subgroupOfPrimitiveMapToOne_iff` for this characterization.

TODO: Generalize to an arbitrary nonzero integer `d`, replacing the hypothesis `p.Prime` with
a coprimality condition and `n / p ^ n.factorization p` with the largest factor of `n` coprime
to `d`. This would require additional Mathlib API for that construction.  -/
DirichletCharacter.subgroupOfPrimitiveMapToOne : (R : Type u_1) →
  [inst : CommMonoidWithZero R] →
    (n : ℕ) → [NeZero n] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → Subgroup (DirichletCharacter R n)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.setOfPred_support : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsHamiltonian → {v | v ∈ p.support} = Set.univ
-- Std.Async.UDP
_private.Std.Async.UDP.0.Std.Async.UDP.Socket.ofNative.injEq : ∀ (native native_1 : Std.Internal.UV.UDP.Socket), ({ native := native } = { native := native_1 }) = (native = native_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_pi_sub : ∀ (θ : Real.Angle), (↑Real.pi - θ).sign = θ.sign
-- Lean.Meta.Sym.Pattern
/-- Returns `true` is `u` has assigned uvars.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.hasAssignedUVars : Array (Option Lean.Level) → Lean.Level → Bool
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.rel.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] {n l : ℕ} (R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin n)),
  sizeOf (FirstOrder.Language.BoundedFormula.rel R ts) = 1 + sizeOf n + sizeOf l + sizeOf R
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.singleRuleTac : Lean.Name → Aesop.RuleTacDescr
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.toSpecMvPoly.eq_1 : ∀ (n : Type u) (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.AffineSpace.toSpecMvPoly n S =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from S)
      (CategoryTheory.Limits.terminal.from (AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))))
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- The injection of `Y` in the optimal coupling between `X` and `Y` is an isometry.  -/
GromovHausdorff.isometry_optimalGHInjr : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y], Isometry (GromovHausdorff.optimalGHInjr X Y)
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- An auxiliary lemma that combines two “exponential of a power” estimates into a similar estimate
on the difference of the functions.  -/
PhragmenLindelof.isBigO_sub_exp_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ},
  (∃ c < a, ∃ B, f =O[Bornology.cobounded ℂ ⊓ l] fun z => Real.exp (B * ‖z‖ ^ c)) →
    (∃ c < a, ∃ B, g =O[Bornology.cobounded ℂ ⊓ l] fun z => Real.exp (B * ‖z‖ ^ c)) →
      ∃ c < a, ∃ B, (f - g) =O[Bornology.cobounded ℂ ⊓ l] fun z => Real.exp (B * ‖z‖ ^ c)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Preregular C] [inst_3 : CategoryTheory.FinitaryExtensive C]
  [h : ∀ {Y X : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Limits.PreservesFiniteProducts F ∧ CategoryTheory.regularTopology.EqualizerCondition F
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.get_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂),
  m₁.get k hk = m₂.get k ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set of differentiability points of a function taking values in a complete space is
Borel-measurable.  -/
measurableSet_of_differentiableAt : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  [inst_5 : MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F], MeasurableSet {x | DifferentiableAt 𝕜 f x}
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_mul : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f : α →₀ M}
  {h₁ h₂ : α → M → N}, (f.prod fun a b => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [Finite ι] (π : BoxIntegral.Prepartition I),
  ∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop,
    π ⊓ BoxIntegral.Prepartition.splitMany I t = (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.Legacy.Iterator.hasNext.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.hasNext = decide (i.byteIdx < s.rawEndPos.byteIdx)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_deriv_one_add_smoothingFn : (deriv fun x => 1 + AkraBazziRecurrence.smoothingFn x) =ᶠ[Filter.atTop] fun x => -x⁻¹ / Real.log x ^ 2
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_le_sub_pow : ∀ (n k : ℕ), n.choose k ≤ (n + 1 - k) ^ k
-- Batteries.Data.List.Basic
List.zipWithLeft'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List β), List.zipWithLeft' f [] x = ([], x)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.rTensorOne'.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S),
  M.rTensorOne' =
    ↑(LinearEquiv.ofEq (M.mulMap (Subalgebra.toSubmodule ⊥)).range M ⋯) ∘ₗ
      (M.mulMap (Subalgebra.toSubmodule ⊥)).rangeRestrict
-- Mathlib.RingTheory.Polynomial.Basic
/-- Given an ideal `I` of `R[X]`, make the `R`-submodule of `I`
consisting of polynomials of degree ≤ `n`.  -/
Ideal.degreeLE : {R : Type u} → [inst : Semiring R] → Ideal (Polynomial R) → WithBot ℕ → Submodule R (Polynomial R)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc : ∀ {n : Type u} {S X Y : AlgebraicGeometry.Scheme} (v : n → ↑(Y.presheaf.obj (Opposite.op ⊤))) (f : X ⟶ Y) (g : Y ⟶ S)
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.AffineSpace n S ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.homOfVector g v) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.AffineSpace.homOfVector (CategoryTheory.CategoryStruct.comp f g)
        (⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) ∘ v))
      h
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_eq : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] {a b : α} {a' b' : ℤ},
  ↑a = a' → ↑b = b' → a = b → a' = b'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_eq_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {he : t.isEmpty = false}, t.minKey he = t.minKey!
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_nonpos_of_nonneg_of_nonpos : ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.mk.injEq : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (base : ↑X)
  (germ : CategoryTheory.ToType (F.stalk base)) (base_1 : ↑X) (germ_1 : CategoryTheory.ToType (F.stalk base_1)),
  ({ base := base, germ := germ } = { base := base_1, germ := germ_1 }) = (base = base_1 ∧ germ ≍ germ_1)
-- Mathlib.Topology.Order
closure_induced : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α} {s : Set α},
  a ∈ closure s ↔ f a ∈ closure (f '' s)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_eq_of_mem_even : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ CliffordAlgebra.evenOdd Q 0 → CliffordAlgebra.involute x = x
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Create a `RefinedDiscrTree` for current module declarations, consisting of all
entries generated by `act` from constants in the current file.
This is called by `addConstToPreDiscrTree`.
 -/
Lean.Meta.RefinedDiscrTree.createModuleDiscrTree : {α : Type} →
  (Lean.Name →
      Lean.ConstantInfo →
        Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
    Lean.CoreM (Lean.Meta.RefinedDiscrTree α)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_comp_lift : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A)
  (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)),
  ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap ∘ₗ CliffordAlgebra.ι Q = f
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.map_fst_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν],
  MeasureTheory.Measure.map Prod.fst (μ.prod ν) = ν Set.univ • μ
-- Lean.Server.FileWorker.RequestHandling
/-- The list of the name components introduced by this namespace command,
in reverse order so that `end` will peel them off from the front.  -/
Lean.Server.FileWorker.NamespaceEntry.name : Lean.Server.FileWorker.NamespaceEntry → List Lean.Name
-- Lean.Message
/-- Helper functions for creating a `MessageData` with the given header and elements.  -/
Lean.toTraceElem : {α : Type} → [Lean.ToMessageData α] → α → optParam Lean.Name (Lean.Name.mkSimple "_") → Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [inst_2 : CategoryTheory.Limits.HasCoend F] {i j : J}
  (f : i ⟶ j) {Z : C} (h : CategoryTheory.Limits.coend F ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F i) h) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) h)
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {β : Type u_2} [inst_3 : CommMonoidWithZero β] [inst_4 : NormalizationMonoid β] [inst_5 : UniqueFactorizationMonoid β]
  {F : Type u_3} [inst_6 : EquivLike F α β] [inst_7 : MulEquivClass F α β] {f : F}
  (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a : α} {q : β}
  (hq : q ∈ UniqueFactorizationMonoid.normalizedFactors (f a)),
  ↑((UniqueFactorizationMonoid.normalizedFactorsEquiv he a).symm ⟨q, hq⟩) = (↑f).symm q
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ] (K : ℝ),
  ∃ C,
    ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),
      ∀ (x : α), ∀ t ≤ K, μ (Metric.closedBall x (t * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_eq_sum_fintype : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : (i : ι) → Zero (β i)]
  [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_4 : AddCommMonoid γ] (v : Π₀ (i : ι), β i)
  {f : (i : ι) → β i → γ}, (∀ (i : ι), f i 0 = 0) → v.sum f = ∑ i, f i (DFinsupp.equivFunOnFintype v i)
-- Mathlib.Order.Max
IsMax.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x → IsMax x.1
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- `sequence 0` identifies to the given functor  -/
CategoryTheory.Functor.ShiftSequence.isoZero : {C : Type u_1} →
  {A : Type u_3} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_3, u_3} A} →
        {F : CategoryTheory.Functor C A} →
          {M : Type u_4} →
            {inst_2 : AddMonoid M} →
              {inst_3 : CategoryTheory.HasShift C M} →
                [self : F.ShiftSequence M] → CategoryTheory.Functor.ShiftSequence.sequence F 0 ≅ F
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.σ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X')
  {n : ℕ} (i : Fin (n + 1)) {Z : C} (h : X'.obj { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (f.app { len := n }) h) =
    CategoryTheory.CategoryStruct.comp (f.app { len := n + 1 }) (CategoryTheory.CategoryStruct.comp (X'.σ i) h)
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- **Alias** of `ChartedSpace.locallyRingedSpace`.

---

A smooth manifold can be considered as a locally ringed space.  -/
IsManifold.locallyRingedSpace : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_1} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_2} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                (M : Type u) → [inst : TopologicalSpace M] → [ChartedSpace HM M] → AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Topology.UniformSpace.Separation
inseparable_iff_ker_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {x y : α}, Inseparable x y ↔ (x, y) ∈ (uniformity α).ker
-- Mathlib.Order.Filter.Basic
Filter.frequently_const : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : Prop}, (∃ᶠ (x : α) in f, p) ↔ p
-- Mathlib.Topology.Algebra.Order.Field
tendsto_const_mul_pow_nhds_iff' : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {n : ℕ} {c d : 𝕜},
  Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (nhds d) ↔ (c = 0 ∨ n = 0) ∧ c = d
-- Mathlib.RingTheory.Multiplicity
Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs : ∀ {a b : ℤ}, FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t₁ t₂ : Set β} {a : α}, a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w}
  [inst_1 : SizeOf C] [inst_2 : (a : C) → SizeOf (ι a)] {X : C} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X)
  (h : ⦃W : C⦄ → (r : W ⟶ X) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W),
  sizeOf (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h) = 1 + sizeOf X + sizeOf hR
-- Mathlib.Data.Finset.Sym
Finset.coe_sym2 : ∀ {α : Type u_1} {m : Finset α}, ↑m.sym2 = (↑m).sym2
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.isSubideal : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (self : hI.SubDPIdeal), self.carrier ≤ I
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.splitter : {n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) →
    (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
      (Unit → motive none) → ((c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)) → motive cOpt
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instInvolutiveNeg : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → InvolutiveNeg (E →ₛₗ.[σ] F)
-- Std.Time.Zoned.TimeZone
Std.Time.instReprTimeZone.repr : Std.Time.TimeZone → ℕ → Std.Format
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.add_comm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.add y) (y.add x)
-- Mathlib.Algebra.Group.EvenFunction
Function.Odd.mul_odd : ∀ {α : Type u_1} [inst : Neg α] {R : Type u_3} [inst_1 : Mul R] {f g : α → R} [inst_2 : HasDistribNeg R],
  Function.Odd f → Function.Odd g → Function.Even (f * g)
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrixLinear_apply : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} (A : Type u_10) {α : Type u_11} {β : Type u_12}
  [inst : Semiring R] [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β]
  [inst_4 : Module R α] [inst_5 : Module S β] [inst_6 : Semiring A] [inst_7 : Module A β] [inst_8 : SMulCommClass S A β]
  (f : α →ₛₗ[σᵣₛ] β), (LinearMap.mapMatrixLinear A) f = f.mapMatrix
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_comp_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  SemidirectProduct.rightHom.comp SemidirectProduct.inl = 1
-- Mathlib.Data.List.Basic
List.head?_append_of_ne_nil : ∀ {α : Type u} (l₁ : List α) {l₂ : List α}, l₁ ≠ [] → (l₁ ++ l₂).head? = l₁.head?
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_apply_of_lt : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ},
  p.natDegree < n → Polynomial.sumIDeriv p = ∑ i ∈ Finset.range n, (⇑Polynomial.derivative)^[i] p
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Premise.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId) = 1 + sizeOf fvarId
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalarsRange₂_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7}
  {P' : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M]
  [inst_4 : Module R M] [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : AddCommMonoid P]
  [inst_8 : Module R P] [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : Module S P]
  [inst_12 : IsScalarTower S R M] [inst_13 : IsScalarTower S R N] [inst_14 : IsScalarTower S R P]
  [inst_15 : AddCommMonoid M'] [inst_16 : Module S M'] [inst_17 : AddCommMonoid N'] [inst_18 : Module S N']
  [inst_19 : AddCommMonoid P'] [inst_20 : Module S P'] [inst_21 : SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N)
  (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P)
  (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range) (m : M') (n : N'),
  k (((i.restrictScalarsRange₂ j k hk B hB) m) n) = (B (i m)) (j n)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.lsingle_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ) (m : M)
  (n : ℕ), ((PolynomialModule.lsingle R i) m).coeff n = if i = n then m else 0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding_injective : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Function.Injective ⇑(NumberField.canonicalEmbedding K)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CasesTypes.mk : Lean.PHashMap Lean.Name Bool → Lean.Meta.Grind.CasesTypes
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.baseChange_integralModel_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (WeierstrassCurve.integralModel R W).baseChange K = W
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits an injective map that preserves
`1`, `*` and `⁻¹` to a group. See note [reducible non-instances].  -/
Function.Injective.group : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : Group M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → Group M₁
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.refl_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] {ρ : Representation A G V} (v : V), (Representation.Equiv.refl ρ) v = v
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_eq_univ_iff : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α},
  ⋃ i, ⋃ j, s i j = Set.univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
-- Mathlib.Topology.Connected.LocallyPathConnected
connectedComponentsEquivZerothHomotopy_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyPathConnectedSpace X] (x : X),
  connectedComponentsEquivZerothHomotopy ⟦x⟧ = ZerothHomotopy.mk x
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe : ∀ {α : Type u} (p q : α → Prop) (a : { x // p x ∧ q x }), ↑↑((Equiv.subtypeSubtypeEquivSubtypeInter p q).symm a) = ↑a
-- Lean.ErrorExplanation
/-- Returns all error explanations with their names, sorted by name.  -/
Lean.getErrorExplanations : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m (Array (Lean.Name × Lean.ErrorExplanation))