mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_nil : ∀ {U : Type u_1} [inst : Quiver U] {u u' : U} (hu : u = u'), Quiver.Path.cast hu hu Quiver.Path.nil = Quiver.Path.nil
-- Mathlib.Algebra.Ring.Defs
/-- A `NonUnitalRing` which `IsMulCommutative` is a `NonUnitalCommRing`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instNonUnitalCommRing : {R : Type v} → [inst : NonUnitalRing R] → [IsMulCommutative R] → NonUnitalCommRing R
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mass_nonzero_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), μ.mass ≠ 0 ↔ μ ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the right.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_right_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
      ((self.mapComp f g').toNatTrans.app X)
-- Lean.Data.DeclarationRange
Lean.instInhabitedDeclarationLocation.default : Lean.DeclarationLocation
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.pos_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {w : NumberField.FinitePlace K} {x : K}, 0 < w x ↔ x ≠ 0
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Small.limitCone_pt : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : Small.{u, max u v} ↑F.sections],
  (CategoryTheory.Limits.Types.Small.limitCone F).pt = Shrink.{u, max u v} ↑F.sections
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], a ∈ m → m.get? a = some (m.get! a)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₂Iso →
          Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.max_le_of_forall_le : ∀ {α : Type u_4} [inst : LinearOrder α] [inst_1 : OrderBot α] (l : Multiset α) (n : α),
  (∀ x ∈ l, x ≤ n) → Multiset.fold max ⊥ l ≤ n
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given a right extension `E` of `F : C ⥤ H` along `L : C ⥤ D` and a functor `G : H ⥤ D'`,
`E.postcompose₂ G` is the extension of `F ⋙ G` along `L` obtained by whiskering by `G`
on the right.  -/
CategoryTheory.Functor.RightExtension.postcompose₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                (L : CategoryTheory.Functor C D) →
                  (F : CategoryTheory.Functor C H) →
                    (G : CategoryTheory.Functor H D') →
                      CategoryTheory.Functor (L.RightExtension F) (L.RightExtension (F.comp G))
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.hasFDerivAt : ∀ {𝕜 : 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 →L[𝕜] F) {x : E}, HasFDerivAt (⇑f) f x
-- Mathlib.FieldTheory.Minpoly.Finite
minpoly.degree_le : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Module.Finite A B] (x : B)
  [Module.Free A B], (minpoly A x).degree ≤ ↑(Module.finrank A B)
-- Mathlib.GroupTheory.HNNExtension
/-- Multiplying `t^u` by `w` in the special case where cancellation happens  -/
HNNExtension.NormalWord.unitsSMulWithCancel : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      ↥A ≃* ↥B →
        {d : HNNExtension.NormalWord.TransversalPair G A B} →
          (u : ℤˣ) → (w : HNNExtension.NormalWord d) → HNNExtension.NormalWord.Cancels u w → HNNExtension.NormalWord d
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) {J' : Type w'} [inst_5 : LinearOrder J'] [inst_6 : OrderBot J']
  [inst_7 : SuccOrder J'] [inst_8 : WellFoundedLT J'] (e : J' ≃o J),
  (c.ofOrderIso e).incl = e.equivalence.functor.whiskerLeft c.incl
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ` for multiset.

Any multiset of at least `2 * n - 1` elements of `ℤ` contains a submultiset of `n` elements whose
sum is divisible by `n`.  -/
Int.erdos_ginzburg_ziv_multiset : ∀ {n : ℕ} (s : Multiset ℤ), 2 * n - 1 ≤ s.card → ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos : ∀ {x y : ℝ*}, ¬x.Infinitesimal → x < 0 → y.InfinitePos → (x * y).InfiniteNeg
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- Constructor for morphisms out of the chosen coend of a functor.  -/
CategoryTheory.Limits.chosenCoend.desc : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} J] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] →
            {X : C} →
              (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X) →
                (∀ ⦃i j : J⦄ (g : i ⟶ j),
                    CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
                      CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) →
                  (CategoryTheory.Limits.chosenCoend F ⟶ X)
-- Lean.Data.NameMap.Basic
Lean.NameSet.instInsertName : Insert Lean.Name Lean.NameSet
-- Init.Data.Array.MinMax
Array.foldl_max_eq_max : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] [Std.Associative max] {xs : Array α} (h : xs ≠ #[]) {a : α},
  Array.foldl max a xs = a ⊔ xs.max h
-- Mathlib.Order.Bounds.Image
image2_upperBounds_lowerBounds_subset_lowerBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → Set.image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.instEmptyCollectionSeenCalls : EmptyCollection Lean.Meta.FunInd.SeenCalls
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α}, (List.map Sigma.fst l).contains k = false → (m.insertMany l).get? k = m.get? k
-- Mathlib.Topology.MetricSpace.IsometricSMul
instIsIsometricVAddForall : ∀ {M : Type u} {ι : Type u_3} {X : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → VAdd M (X i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricVAdd M (X i)], IsIsometricVAdd M ((i : ι) → X i)
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.instMeasureSpaceElemReal : MeasureTheory.MeasureSpace ↑unitInterval
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.disjoint_iff : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {a b : ↥L}, Disjoint a b ↔ Disjoint ↑a ↑b
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- See Note [custom simps projection]  -/
LieDerivation.Simps.apply : {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] → LieDerivation R L M → L → M
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withEqs.go : {α : Type} →
  Array Lean.Expr →
    Array Lean.Expr →
      Array Lean.Meta.Match.DiscrInfo → (Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.termSX' : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.rid_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (TensorProduct.rid R M).symm m = m ⊗ₜ[R] 1
-- Batteries.Recycling.RBTree.Alter
/-- The ordering invariant for a `Path`.  -/
RBTree.RBNode.Path.Ordered : {α : Type u_1} → (α → α → Ordering) → RBTree.RBNode.Path α → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.toLp_def : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  (f : C(α, E)),
  (ContinuousMap.toLp p μ 𝕜) f =
    (BoundedContinuousFunction.toLp p μ 𝕜) ((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ι_normalizedChainComplexMap_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {n : ℕ}
  (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (Y.normalizedChainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x)
      (CategoryTheory.CategoryStruct.comp ((SSet.normalizedChainComplexMap f R).f n) h) =
    CategoryTheory.CategoryStruct.comp
      (Y.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)) h
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural inclusion
ordered homomorphism from N to the lexicographic M ×ₗ N.  -/
OrderAddMonoidHom.inrₗ : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] →
      [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → β →+o Lex (α × β)
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_toUSize : ∀ (n : UInt32), n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjMap_comp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) {F₁ F₂ F₃ : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F₁] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W F₂]
  [inst_4 : CategoryTheory.Limits.HasWeightedLimit W F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃),
  W.weightedLimObjMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (W.weightedLimObjMap f) (W.weightedLimObjMap g)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M),
  HasMFDerivAt% id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).K = S.X₂
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.uSwitch.eq_1 : FintypeCat.uSwitch =
  { obj := fun X => FintypeCat.of (ULift.{v, 0} (Fin (Fintype.card X.obj))),
    map := fun {X Y} f =>
      FintypeCat.homMk
        (ULift.up ∘
          ⇑(Fintype.equivFin Y.obj) ∘
            ⇑(CategoryTheory.ConcreteCategory.hom f.hom) ∘ ⇑(Fintype.equivFin X.obj).symm ∘ ULift.down),
    map_id := FintypeCat.uSwitch._proof_2, map_comp := @FintypeCat.uSwitch._proof_4 }
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.smul_sphere : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ), c • Metric.sphere x r = Metric.sphere (c • x) r
-- Mathlib.Logic.Equiv.Defs
/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse.  -/
«term_≃_» : Lean.TrailingParserDescr
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.eraseDupsBy_loop_cons : ∀ {α : Type u_1} {as bs : List α} {r : α → α → Bool},
  List.eraseDupsBy.loop r as bs = bs.reverse ++ List.eraseDupsBy.loop r (List.filter (fun a => !bs.any (r a)) as) []
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- **Alias** of `multipliable_of_hasFiniteMulSupport`. -/
multipliable_of_finite_mulSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [L.HasSupport], Function.HasFiniteMulSupport f → Multipliable f L
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The coinduced continuous representation where the action of `H` is defined by
`h ↦ f ↦ f ∘ (· * h)`.  -/
ContRepresentation.coind : {R : Type u_1} →
  {V : Type u_3} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : IsTopologicalAddGroup V] →
            [inst_4 : Module R V] →
              {G : Type u_7} →
                {H : Type u_8} →
                  [inst_5 : Group G] →
                    [inst_6 : TopologicalSpace G] →
                      [inst_7 : TopologicalSpace R] →
                        [inst_8 : ContinuousSMul R V] →
                          [inst_9 : Group H] →
                            [inst_10 : TopologicalSpace H] →
                              (φ : G →ₜ* H) →
                                [IsTopologicalGroup H] →
                                  (π : ContRepresentation R G V) →
                                    ContRepresentation R H ↥(ContRepresentation.coindV φ π)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to `S.L₂'` which is
`S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorL₂' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- If we rewrite into this expression, then the goal will be solved.  -/
Mathlib.Tactic.ClickSuggestions.RwInfo.rflTarget? : Mathlib.Tactic.ClickSuggestions.RwInfo → Option Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The underlying oplax natural transformation of a strong natural transformation.  -/
CategoryTheory.Oplax.StrongTrans.toOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Oplax.StrongTrans F G → CategoryTheory.Oplax.OplaxTrans F G
-- Lean.Elab.Term.TermElabM
/-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation.  -/
Lean.Elab.Tactic.TacticFinishedSnapshot.moreSnaps : Lean.Elab.Tactic.TacticFinishedSnapshot → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_of_pow_prime_eq_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {p : ℕ} [Fact (Nat.Prime p)],
  σ ^ p = 1 → σ.cycleType = Multiset.replicate σ.cycleType.card p
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.isEqvAux.match_1.eq_1 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (x : 0 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Solvers.mergeTerms : Lean.Meta.Grind.ENode → Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Lean.Meta.Grind.PendingSolverPropagations
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.nonempty : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  [Mn : Nonempty M], L.ElementarilyEquivalent M N → Nonempty N
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_le_aleph_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} c ≤ Cardinal.aleph ↑n ↔ c ≤ Cardinal.aleph ↑n
-- Mathlib.Topology.CompactOpen
ContinuousMap.instR1Space : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [R1Space Y], R1Space C(X, Y)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Transport evidence that a right lift is a Kan lift across an isomorphism of lifts.  -/
CategoryTheory.Bicategory.RightLift.IsKan.ofIsoKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} → {g : c ⟶ a} → {s t : CategoryTheory.Bicategory.RightLift f g} → s.IsKan → (s ≅ t) → t.IsKan
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instModuleRepr : {R : Type u_1} → [inst : Ring R] → (x : FGModuleRepr R) → Module R x.repr
-- Mathlib.FieldTheory.Fixed
prodXSubSMul.eq_1 : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Fintype G] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : MulSemiringAction G R] (x : R),
  prodXSubSMul G R x = ∏ g, (Polynomial.X - Polynomial.C (MulAction.ofQuotientStabilizer G x g))
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A partial map restricts to a map from `Spec K(X)`.  -/
AlgebraicGeometry.Scheme.PartialMap.fromFunctionField : {X Y : AlgebraicGeometry.Scheme} →
  [inst : IrreducibleSpace ↥X] → X.PartialMap Y → (AlgebraicGeometry.Spec X.functionField ⟶ Y)
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in well-founded recursive functions recursing over a productive
iterator (see also `Productive`).
 -/
Std.Iter.finitelyManySkips : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.Iterators.Productive α Id] → Std.Iter β → Std.IterM.TerminationMeasures.Productive α Id
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedInjectiveInfo.default : Lean.Meta.Grind.InjectiveInfo
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Matrix.SpecialLinearGroup.toGL_mem_center_iff : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (g : Matrix.SpecialLinearGroup n R),
  Matrix.SpecialLinearGroup.toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (Matrix.SpecialLinearGroup n R)
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- Notation for the identity morphism in a category.  -/
CategoryTheory.«term𝟙rq» : Lean.ParserDescr
-- Lean.Parser.Command
Lean.Parser.Command.synth : Lean.Parser.Parser
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sub_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree (f - g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraEquivOfIsoMonads_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂),
  (CategoryTheory.Monad.algebraEquivOfIsoMonads h).functor = CategoryTheory.Monad.algebraFunctorOfMonadHom h.inv
-- Init.Data.Slice.Operations
/-- Computes the slice of a `Slice`. Use `Slice.size` instead.  -/
Std.Slice.SliceSize.size : {γ : Type u} → [self : Std.Slice.SliceSize γ] → Std.Slice γ → ℕ
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkConsistentParentChildLinks.err : Lean.CoreM Unit
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.even_finrank_of_not_isUnramifiedIn : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  {w : NumberField.InfinitePlace k}, ¬NumberField.InfinitePlace.IsUnramifiedIn K w → Even (Module.finrank k K)
-- Mathlib.Order.Atoms
/-- Dual variant of `SetLike.covBy_iff`  -/
SetLike.covBy_iff' : ∀ {A : Type u_4} {B : Type u_5} [inst : PartialOrder A] [inst_1 : SetLike A B] [IsConcreteLE A B] {K L : A},
  K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.apply_eq_apply_iff_rel : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a b : α}, P.IsRepFun f → a ∈ u → (f a = f b ↔ P.Rel a b)
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.toByCasesSubgoal : Lean.Meta.CasesSubgoal → Lean.MetaM Lean.Meta.ByCasesSubgoal
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)),
  (CategoryTheory.Over.ConstructProducts.conesEquiv B F).counitIso =
    CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F
-- Init.Data.Array.Basic
/-- Returns the first `n` elements of an array. The resulting array is produced by repeatedly calling
`Array.pop`. If `n` is greater than the size of the array, it is returned unmodified.

If the reference to the array is unique, then this function uses in-place modification.

Examples:
* `#[0, 1, 2, 3, 4].shrink 2 = #[0, 1]`
* `#[0, 1, 2, 3, 4].shrink 0 = #[]`
* `#[0, 1, 2, 3, 4].shrink 10 = #[0, 1, 2, 3, 4]`
 -/
Array.shrink : {α : Type u} → Array α → ℕ → Array α
-- Init.Data.Int.Lemmas
Int.one_mul : ∀ (a : ℤ), 1 * a = a
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.mk_coe : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →⋆ₙ+* B) (h₁ : ∀ (x y : A), f (x * y) = f x * f y)
  (h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
        { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y)
  (h₄ :
    ∀ (a : A),
      { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
        star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)),
  { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } = f