mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (x : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_2 size k v r x
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsNontrivial.exists_lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [ValuativeRel.IsNontrivial R], ∃ γ, 0 < γ ∧ γ < 1
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- The list of vertices in a path, including the start and end vertices.  -/
Quiver.Path.vertices : {V : Type u_1} → [inst : Quiver V] → {a b : V} → Quiver.Path a b → List V
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.revSkipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_mulVec_const_apply_of_regular : ∀ {α : Type u_1} {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] {d : ℕ} {a : α},
  G.IsRegularOfDegree d → ∀ {v : V}, (SimpleGraph.adjMatrix α G).mulVec (Function.const V a) v = ↑d * a
-- Mathlib.Data.TypeVec
/-- arrow in the category of `TypeVec`  -/
MvFunctor.«term_⟹_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Matrix.Determinant.Misc
/-- Let `M` be a `(n+1) × n` matrix whose column sums to zero. Then all the matrices obtained by
deleting one column have the same determinant up to a sign.  -/
Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin (n + 1)) R),
  (∀ (i : Fin n), ∑ j, M i j = 0) →
    ∀ (j₁ j₂ : Fin (n + 1)),
      (M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det
-- Mathlib.Algebra.Order.Group.MinMax
abs_min_sub_min_le_max : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c d : α),
  |min a b - min c d| ≤ max |a - c| |b - d|
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- This lemma should be erased, or at least burn in hell, as it uses bad defeq: the left model
with corners is for `E times F`, the right one for `ModelProd E F`, and there's a good reason
we are distinguishing them.  -/
modelWithCornersSelf_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  modelWithCornersSelf 𝕜 (E × F) = (modelWithCornersSelf 𝕜 E).prod (modelWithCornersSelf 𝕜 F)
-- Init.Data.SInt.Lemmas
Int64.succ_mul : ∀ {a b : Int64}, (a + 1) * b = a * b + b
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.φ.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (s : Finset S),
  PolynomialLaw.φ R s = MvPolynomial.aeval fun n => ↑(s.equivFin.symm n)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α),
  Std.DHashMap.Internal.AssocList.contains a Std.DHashMap.Internal.AssocList.nil = false
-- Std.Data.TreeMap.Raw.Iterator
/-- Returns a finite iterator over the values of a tree map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeMap.Raw.valuesIter : {α β : Type u} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.Iter β
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_14 : HSub Std.Time.Second.Offset Std.Time.Minute.Offset Std.Time.Second.Offset
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_gcd_helper_2 : ∀ (d x y a b : ℕ), x % d = 0 → y % d = 0 → x * a = y * b + d → x.gcd y = d
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.instIsProbabilityMeasureProdCompProdOfIsMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ],
  MeasureTheory.IsProbabilityMeasure (μ.compProd κ)
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.ext : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {S T : StarSubsemiring R},
  (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.RingTheory.PrincipalIdealDomain
Ideal.span_singleton_generator : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R) [inst_1 : Submodule.IsPrincipal I],
  Ideal.span {Submodule.IsPrincipal.generator I} = I
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- Any chosen pullback of a composite of morphisms is naturally isomorphic to the composition of
chosen pullback functors.  -/
CategoryTheory.ChosenPullbacksAlong.pullbackComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
            [inst_2 : CategoryTheory.ChosenPullbacksAlong g] →
              [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)] →
                CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.comp f g) ≅
                  (CategoryTheory.ChosenPullbacksAlong.pullback g).comp (CategoryTheory.ChosenPullbacksAlong.pullback f)
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.continuousAddCharEquiv_symm_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] {r : R}
  (hr : Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0)),
  ↑((PadicInt.continuousAddCharEquiv p R).symm ⟨r, hr⟩) = PadicInt.addChar_of_value_at_one r hr
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below : {B : Type u} →
  [inst : Quiver B] →
    {motive :
        {a b : CategoryTheory.FreeBicategory B} →
          {f g : a ⟶ b} →
            (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop} →
      {a b : CategoryTheory.FreeBicategory B} →
        {f g : a ⟶ b} →
          {a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g} → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsNonneg.nonneg : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {I₁ I₂ : R →+* R} [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R}, B.IsNonneg → ∀ (x : M), 0 ≤ (B x) x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {m n : ℕ} (s : Affine.Simplex k P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).interior = s.interior
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.amalgamate.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySheafFor F)
  (x : (i : E.I₀) → F.obj (Opposite.op (E.X i)))
  (hc :
    ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
      (CategoryTheory.ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) =
        (CategoryTheory.ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)),
  h.amalgamate x hc = ⋯.amalgamate ⋯.familyOfElements ⋯
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (f : ι → NonemptyInterval α) (s : Finset ι), (∑ i ∈ s, f i).length = ∑ i ∈ s, (f i).length
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)] {f : Option (β k) → Option (β k)},
  (t.alter k f).get! k = (f (t.get? k)).get!
-- Lean.InternalExceptionId
/-- Internal exception identifier  -/
Lean.InternalExceptionId : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.topIso_hom : ∀ (X : SSet), (SSet.Subcomplex.topIso X).hom = ⊤.ι
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finsum_eq_finsetSum_of_support_subset`. -/
finsum_eq_finset_sum_of_support_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Finset α},
  Function.support f ⊆ ↑s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.Hom.hom_hom_zpow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X]
  (f : G ⟶ H) (n : ℤ), (f ^ n).hom.hom = f.hom.hom ^ n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_comp_d₁₀_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G × G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) x) =
    0
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (c • f) x
-- Mathlib.Order.WithBot
WithBot.unbot_lt_unbot_iff : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥), x.unbot hx < y.unbot hy ↔ x < y
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.instAddActionQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : AddMonoid S] → [inst_1 : AddAction S M] → (c : VAddCon S M) → AddAction S (VAddCon.Quotient M c)
-- Mathlib.Algebra.Category.Grp.Basic
/-- An alias for `CommGrpCat.{max u v}`, to deal around unification issues.  -/
CommGrpMax : Type ((max u1 u2) + 1)
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.lparams : Lean.Elab.ComputedFields.Context → List Lean.Level
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.map_cast_binomial_singleton : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R]
  (n k : ℕ) (p : ↑unitInterval),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) {↑k} =
    ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))
-- Mathlib.Analysis.Seminorm
Seminorm.pullback_apply : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (p : Seminorm 𝕜₂ E₂),
  (Seminorm.pullback f) p = p.comp f
-- Mathlib.MeasureTheory.VectorMeasure.AddContent
/-- A finitely additive vector measure which is dominated by a finite positive measure is in
fact countably additive.  -/
MeasureTheory.VectorMeasure.of_additive_of_le_measure : {α : Type u_1} →
  {hα : MeasurableSpace α} →
    {E : Type u_2} →
      [inst : NormedAddCommGroup E] →
        {μ : MeasureTheory.Measure α} →
          (m : Set α → E) →
            (∀ (s : Set α), ‖m s‖ₑ ≤ μ s) →
              [MeasureTheory.IsFiniteMeasure μ] →
                (∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) →
                  (∀ (s : Set α), ¬MeasurableSet s → m s = 0) → MeasureTheory.VectorMeasure α E
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
/-- The injection `(x₁, x₂) ↦ x₁` is always an `r`-coloring of a `completeEquipartiteGraph r ·`.  -/
SimpleGraph.Coloring.completeEquipartiteGraph : {r t : ℕ} → (SimpleGraph.completeEquipartiteGraph r t).Coloring (Fin r)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- An object in `Type u` is initial if and only if it is empty.  -/
CategoryTheory.Limits.Types.initial_iff_empty : ∀ (X : Type u), Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty X
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesLimitNatIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape J G] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C),
  (CategoryTheory.preservesLimitNatIso G).hom.app X = (CategoryTheory.preservesLimitIso G X).hom
-- Init.Data.List.Nat.Range
List.mk_add_mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {k i : ℕ} {x : α} {l : List α}, (x, k + i) ∈ l.zipIdx k ↔ l[i]? = some x
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS'.visitAppBeta : Array Lean.Expr → Lean.Expr → Lean.Expr → Array Lean.Expr → ℕ → Bool → Lean.Meta.Sym.M✝ Lean.Expr
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_div_union_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
-- Mathlib.Order.MinMax
min_lt_min_right_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min a b < min a c ↔ b < c ∧ b < a
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanImportClosureParams.toJson : Lean.Lsp.LeanImportClosureParams → Lean.Json
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.fst_compEquiv : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  LinearMap.fst T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) ∘ₗ
      ↑(Algebra.Generators.CotangentSpace.compEquiv Q P) =
    Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.isRepresentation.toEnd_exists_mem_ideal : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤)
  (f : Module.End R M) (I : Ideal R),
  LinearMap.range f ≤ I • ⊤ → ∃ M_1, (Matrix.isRepresentation.toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.prod_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring R),
  s.prod ⊤ = Subsemiring.comap (RingHom.fst R S) s
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.erase_dup c = Lean.Meta.Grind.AC.EqCnstrProof.erase_dup c_1 → c = c_1
-- Mathlib.Algebra.Group.Hom.Instances
/-- `ZeroHom M N` is an `AddMonoid` if `N` is.  -/
ZeroHom.instAddMonoid : {M : Type uM} → {N : Type uN} → [inst : Zero M] → [inst_1 : AddMonoid N] → AddMonoid (ZeroHom M N)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instIsTrivialOfOfIsTrivial : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {V : Type w} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [ρ.IsTrivial], (Rep.of ρ).IsTrivial
-- Init.Data.BitVec.Lemmas
BitVec.le_toInt_shiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, -2 ^ (w - 1) ≤ x.toInt >>> n
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00PV](https://stacks.math.columbia.edu/tag/00PV) -/
exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R),
  φ.IsIntegralElem t → φ p * t ∈ φ.range → ∃ q n, IsIntegral R (p.leadingCoeff ^ n • t - φ q)
-- Mathlib.GroupTheory.SemidirectProduct
/-- The semidirect product of groups `N` and `G`, given a map `φ` from `G` to the automorphism
group of `N`. It is the product of sets with the group operation
`⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩`  -/
«term_⋊[_]_» : Lean.TrailingParserDescr
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray : {α : Type u} → Std.Rcc.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `initial_comp` below.  -/
CategoryTheory.Functor.initial_equivalence_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.Initial], (F.comp G).Initial
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
/-- **Alias** of `ModuleCat.projectiveDimension_eq_of_semiLinearEquiv`. -/
CategoryTheory.projectiveDimension_eq_of_semiLinearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] [Small.{v', u'} R'] (e : R ≃+* R')
  {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N),
  CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N
-- Init.Data.Vector.Basic
Vector.instGetElemNatLt : {α : Type u_1} → {n : ℕ} → GetElem (Vector α n) ℕ α fun x i => i < n
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_uIoc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.uIoc i j = Set.uIoc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- `MulActionHom` maps `fixedBy` to `fixedBy`.  -/
MulActionHom.map_mem_fixedBy : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid G] [inst_1 : MulAction G A] [inst_2 : MulAction G B]
  (f : A →ₑ[id] B) {g : G} {a : A}, a ∈ MulAction.fixedBy A g → f a ∈ MulAction.fixedBy B g
-- Lean.Compiler.LCNF.Types
/-- Return `true` if `type` is a predicate.
Examples: `Nat → Prop`, `Prop`, `Int → Bool → Prop`.
 -/
Lean.Compiler.LCNF.isPredicateType : Lean.Expr → Bool
-- Mathlib.Topology.Connected.Basic
IsPreconnected.gt_of_ne : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {s : Set α} [inst_1 : LinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β},
  IsPreconnected s → ContinuousOn f s → (∀ x ∈ s, f x ≠ b) → (∃ x ∈ s, f x < b) → ∀ {x : α}, x ∈ s → f x < b
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Exception.revertFailure.sizeOf_spec : ∀ (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (toRevert : Array Lean.Expr) (varName : String),
  sizeOf (Lean.MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert varName) =
    1 + sizeOf mctx + sizeOf lctx + sizeOf toRevert + sizeOf varName
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Interval integrability is invariant when functions change along discrete sets.  -/
intervalIntegrable_congr_codiscreteWithin : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} [MeasureTheory.NullSingletonClass μ],
  f =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] g → (IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b)
-- Mathlib.Algebra.Group.Defs
Group.inv_mul_cancel : ∀ {G : Type u} [self : Group G] (a : G), a⁻¹ * a = 1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData.mk.inj : ∀ {errors errors_1 : IO.Ref (Array Lean.Meta.RefinedDiscrTree.ImportFailure✝)},
  { errors := errors } = { errors := errors_1 } → errors = errors_1
-- Init.Data.List.Sublist
List.prefix_filter_iff : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₂ <+: List.filter p l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = List.filter p l
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivCongrLeft_symm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β),
  (Finsupp.equivCongrLeft f).symm = Finsupp.equivCongrLeft f.symm
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.f_int.eq_1 : ∀ (k : ℕ) (a t : ℝ) (n : ℤ), HurwitzKernelBounds.f_int k a t n = |↑n + a| ^ k * Real.exp (-Real.pi * (↑n + a) ^ 2 * t)
-- Mathlib.Order.WithBot
/-- Specialization of `Option.getD` to values in `WithBot α` that respects API boundaries.  -/
WithBot.unbotD : {α : Type u_1} → α → WithBot α → α
-- Mathlib.LinearAlgebra.Matrix.Permutation
Function.fixedPoints.eq_1 : ∀ {α : Type u_1} (f : α → α), Function.fixedPoints f = {x | Function.IsFixedPt f x}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.forInUncurried_eq_forIn_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Const.forInUncurried f init t = forIn (Std.DTreeMap.Const.toArray t) init f
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.wellFounded_of_productive : ∀ {γ : Type u_1} {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.IteratorLoop α m m]
  [Std.Iterators.Productive α m] {P : β → γ → ForInStep γ → Prop},
  (∀ {b : β} {g : γ} {s : ForInStep γ},
      P b g s →
        (match s with
          | ForInStep.done a => true
          | x => false) =
          true) →
    Std.IteratorLoop.WellFounded α m P
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.lim.π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] (j : J) (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.lim.π j).app F = CategoryTheory.Limits.limit.π F j