mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Non-unital and non-associative convolution semiring structure on linear maps from a
coalgebra to a non-unital non-associative algebra.  -/
LinearMap.convNonUnitalNonAssocSemiring : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : AddCommMonoid C] →
                  [inst_6 : Module R C] → [CoalgebraStruct R C] → NonUnitalNonAssocSemiring (WithConv (C →ₗ[R] A))
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- An additive monoid homomorphism `f : M →+ N` with a left-inverse `g : N → M` defines an
additive equivalence between `M` and `f.mrange`. This is a bidirectional version of
`AddMonoidHom.mrangeRestrict`.  -/
AddEquiv.ofLeftInverse' : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (f : M →+ N) → {g : N → M} → Function.LeftInverse g ⇑f → M ≃+ ↥(AddMonoidHom.mrange f)
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.TacticM.runCore' : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.Context → Lean.Elab.Tactic.State → Lean.Elab.TermElabM α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Types.End
/-- A `ChosenCoends` instance on `Type` given by the explicit quotient construction above.  -/
CategoryTheory.Limits.instChosenCoendsType : CategoryTheory.Limits.ChosenCoends.{v, u, max u w, max (u + 1) (w + 1)} (Type (max w u))
-- Mathlib.Algebra.Order.Group.Abs
le_abs' : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
  a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.norm.eq_1 : ∀ (e : Int.Internal.Linear.Expr), e.norm = e.toPoly'.norm
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_f_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ),
  CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) ((AlgebraicTopology.DoldKan.P q).f n) =
    (AlgebraicTopology.DoldKan.P q).f n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Data.Holor
_private.Mathlib.Data.Holor.0.Holor.«term_⊗_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instDistribMulActionOfIsScalarTower : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Monoid S] →
        [inst_2 : DistribMulAction S R] → [IsScalarTower S R R] → (f : Polynomial R) → DistribMulAction S (AdjoinRoot f)
-- Batteries.Data.Vector.Lemmas
Vector.scanl_reverse : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  Vector.scanl f init as.reverse = (Vector.scanr (flip f) init as).reverse
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
SecondCountableTopologyEither.mk : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  SecondCountableTopology α ∨ SecondCountableTopology β → SecondCountableTopologyEither α β
-- Init.Data.Nat.Div.Basic
Nat.mod_def : ∀ (m k : ℕ), m % k = m - k * (m / k)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_head : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} {w : Monoid.CoprodI.Word M},
  ((Monoid.CoprodI.Word.equivPair i) w).head =
    if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- For a manifold `N` and a `C^n` homomorphism `φ` between Lie groups `G'`, `G''`, the
'left-composition-by-`φ`' group homomorphism from `C^n⟮I, N; I', G'⟯` to `C^n⟮I, N; I'', G''⟯`.  -/
ContMDiffMap.compLeftMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            (N : Type u_6) →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {E'' : Type u_7} →
                                    [inst_9 : NormedAddCommGroup E''] →
                                      [inst_10 : NormedSpace 𝕜 E''] →
                                        {H'' : Type u_8} →
                                          [inst_11 : TopologicalSpace H''] →
                                            {I'' : ModelWithCorners 𝕜 E'' H''} →
                                              {n : WithTop ℕ∞} →
                                                {G' : Type u_10} →
                                                  [inst_12 : Monoid G'] →
                                                    [inst_13 : TopologicalSpace G'] →
                                                      [inst_14 : ChartedSpace H' G'] →
                                                        [inst_15 : ContMDiffMul I' n G'] →
                                                          {G'' : Type u_11} →
                                                            [inst_16 : Monoid G''] →
                                                              [inst_17 : TopologicalSpace G''] →
                                                                [inst_18 : ChartedSpace H'' G''] →
                                                                  [inst_19 : ContMDiffMul I'' n G''] →
                                                                    (φ : G' →* G'') →
                                                                      ContMDiff I' I'' n ⇑φ →
                                                                        ContMDiffMap I I' N G' n →*
                                                                          ContMDiffMap I I'' N G'' n
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.toPartialEquiv : {𝕜 : 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] → ModelWithCorners 𝕜 E H → PartialEquiv H E
-- Init.Data.BitVec.Lemmas
BitVec.smod.eq_1 : ∀ {m : ℕ} (x y : BitVec m),
  x.smod y =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      have u := x.umod y.neg;
      if u = BitVec.zero m then u else u.add y
    | true, false =>
      have u := x.neg.umod y;
      if u = BitVec.zero m then u else y.sub u
    | true, true => (x.neg.umod y.neg).neg
-- Mathlib.Algebra.Order.Module.Field
OrderIso.smulRightDual_apply : ∀ {𝕜 : Type u_1} (G : Type u_2) [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [inst_5 : IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜}
  [inst_7 : PosSMulMono 𝕜 G] (ha : a < 0) (a_1 : G), (OrderIso.smulRightDual G ha) a_1 = a • OrderDual.toDual a_1
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instMulZeroOneClass : {α : Type u_1} → [MulZeroOneClass α] → MulZeroOneClass αᵒᵈ
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.isRightDerivabilityStructure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C], (HomotopyCategory.Plus.localizerMorphism C).IsRightDerivabilityStructure
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The functorial infimum on `MonoOver A` descends to an infimum on `Subobject A`.  -/
CategoryTheory.Subobject.inf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasPullbacks C] →
      {A : C} →
        CategoryTheory.Functor (CategoryTheory.Subobject A)
          (CategoryTheory.Functor (CategoryTheory.Subobject A) (CategoryTheory.Subobject A))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp}, (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_map : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} (A : Matrix m n R) (f : R → S), (A.map f).vec = f ∘ A.vec
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Given two disjoint closed sets `s, t` in a Hausdorff normal σ-compact finite-dimensional
manifold `M`, there exists a smooth function `f : M → [0,1]` that vanishes in a neighbourhood of `s`
and is equal to `1` in a neighbourhood of `t`.  -/
exists_contMDiffMap_zero_one_nhds_of_isClosed : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] {n : ℕ∞} [T2Space M] [NormalSpace M] [SigmaCompactSpace M]
  {s t : Set M},
  IsClosed s →
    IsClosed t →
      Disjoint s t →
        ∃ f, (∀ᶠ (x : M) in nhdsSet s, f x = 0) ∧ (∀ᶠ (x : M) in nhdsSet t, f x = 1) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
-- Mathlib.NumberTheory.Pell
/-- If a solution has `x > 1`, then `d` is positive.  -/
Pell.Solution₁.d_pos_of_one_lt_x : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 1 < a.x → 0 < d
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_nnratCast : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : NNRatCast R]
  (q : ℚ≥0), (HahnSeries.single 0) ↑q = ↑q
-- Mathlib.Data.Set.Insert
Set.mem_insert : ∀ {α : Type u_1} (x : α) (s : Set α), x ∈ insert x s
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.inclusion_inj : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) {x y : ↥H},
  (AddSubgroup.inclusion h) x = (AddSubgroup.inclusion h) y ↔ x = y
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.getNormTheorems : Lean.MetaM Lean.Meta.SimpTheorems
-- Init.Core
/-- An irreflexive relation satisfies `¬ r a a`.  -/
Std.Irrefl.irrefl : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Irrefl r] (a : α), ¬r a a
-- Mathlib.Algebra.GradedMonoid
SetLike.GradedOne.mk : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : One R] [inst_2 : Zero ι] {A : ι → S},
  1 ∈ A 0 → SetLike.GradedOne A
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.tensorUnit_isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A],
  CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A))
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.extendLe_apply_self : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) (x : ↑(hs.extend hst)),
  (Module.Basis.extendLe hs hst ht) x = ↑x
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.subtypePermOfFintype_one : ∀ {α : Type u} (p : α → Prop) [inst : Finite { x // p x }] (h : ∀ (x : α), p x → p (1 x)),
  Equiv.Perm.subtypePermOfFintype 1 h = 1
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (Φ : J.Point),
  CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber (CategoryTheory.CategoryStruct.id Φ) =
    CategoryTheory.CategoryStruct.id Φ.sheafFiber
-- Std.Sync.Broadcast
Std.Broadcast.Error.ofNat : ℕ → Std.Broadcast.Error
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.coneEquiv.inverse.obj t).pt.right.as = PUnit.unit
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.MonoidalCategory.curriedTensorPreFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.MonoidalCategory.curriedTensorPreFunctor.obj F = CategoryTheory.MonoidalCategory.curriedTensorPre F
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mk.sizeOf_spec : ∀ {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SizeOf R] [inst_2 : SizeOf M] (carrier : Set M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier),
  sizeOf { carrier := carrier, smul_mem' := smul_mem' } = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).minKey? = t.minKey?
-- Mathlib.Data.List.MinMax
List.Perm.minimum_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {l l' : List α}, l.Perm l' → l.minimum = l'.minimum
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Finset.multipliable : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
  Multipliable (f ∘ Subtype.val)
-- Mathlib.Order.Filter.Map
Filter.map_compose : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : α → β} {m' : β → γ},
  Filter.map m' ∘ Filter.map m = Filter.map (m' ∘ m)
-- Mathlib.Topology.Algebra.Star
ContinuousWithinAt.star : ∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R]
  [inst_3 : TopologicalSpace α] {f : α → R} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => star (f x)) s x
-- Mathlib.Topology.Homotopy.Basic
/-- value of the homotopy at 0  -/
ContinuousMap.HomotopyLike.map_zero_left : ∀ {X : outParam (Type u_3)} {Y : outParam (Type u_4)} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {F : Type u_5} {f₀ f₁ : outParam C(X, Y)} {inst_2 : FunLike F (↑unitInterval × X) Y}
  [self : ContinuousMap.HomotopyLike F f₀ f₁] (f : F) (x : X), f (0, x) = f₀ x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_eq_top : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.radical = ⊤ ↔ I = ⊤
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- Multiplication preserves finiteness.  -/
Set.fintypeMul : {α : Type u_2} → [inst : Mul α] → [DecidableEq α] → (s t : Set α) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s * t)
-- Mathlib.RingTheory.Regular.IsSMulRegular
biUnion_associatedPrimes_eq_compl_regular : ∀ (R : Type u_1) (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsNoetherianRing R], ⋃ p ∈ associatedPrimes R M, ↑p = {r | IsSMulRegular M r}ᶜ
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.iff_eq_one : ∀ {M : Type u_1} [inst : CancelMonoid M] {a : M}, IsIdempotentElem a ↔ a = 1
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃` and a map `p : I × J → K`, this is the
functor `GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject K C₃` sending
`X : GradedObject I C₁` and `Y : GradedObject J C₂` to the `K`-graded object sending
`k` to the coproduct of `(F.obj (X i)).obj (Y j)` for `p ⟨i, j⟩ = k`.  -/
CategoryTheory.GradedObject.mapBifunctorMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {I : Type u_4} →
                {J : Type u_5} →
                  {K : Type u_6} →
                    (p : I × J → K) →
                      [∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
                            (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] →
                        CategoryTheory.Functor (CategoryTheory.GradedObject I C₁)
                          (CategoryTheory.Functor (CategoryTheory.GradedObject J C₂) (CategoryTheory.GradedObject K C₃))
-- Std.Time.Time.Unit.Second
Std.Time.Second.instLTOrdinal : {leap : Bool} → LT (Std.Time.Second.Ordinal leap)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.lift_comp_one_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.MonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.MonObj.one) g)
      CategoryTheory.MonObj.mul =
    g
-- Init.Grind.Config
/-- Maximum number of steps performed by the `ac` solver.
A step is counted whenever one AC equation is used to simplify another.
For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
used to simplify the second to `max w y = x`.
 -/
Lean.Grind.Config.acSteps : Lean.Grind.Config → ℕ
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given an injective `AddCommMonoid` homomorphism `g : M →+ P`, and a
submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
to the localization of `P` at `g S`, is injective.  -/
AddSubmonoid.LocalizationMap.map_injective_of_injective : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {Q : Type u_4} [inst_3 : AddCommMonoid Q],
  Function.Injective ⇑g → ∀ (k : (AddSubmonoid.map g S).LocalizationMap Q), Function.Injective ⇑(f.map ⋯ k)
-- Batteries.Data.List.Lemmas
List.swap_swap_flip : ∀ {α : Type u_1} {xs : List α} {i j : ℕ}, (xs.swap i j).swap j i = xs
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem' : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ)
  (a b : (x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal),
  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred a →
    (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred b →
      (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred (a * b)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.fst_darts_getElem : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (hi : i < p.darts.length),
  p.darts[i].toProd.1 = p.support.dropLast[i]
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is
canonically isomorphic to the product of its localizations at the (finitely many) maximal ideals.  -/
MaximalSpectrum.toPiLocalizationEquiv : (R : Type u) → [inst : CommSemiring R] → [DiscreteTopology (PrimeSpectrum R)] → R ≃ₐ[R] MaximalSpectrum.PiLocalization R
-- Init.Data.Vector.Lemmas
Vector.mem_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {size : xs.size = n} {a : α}, a ∈ Vector.mk xs size ↔ a ∈ xs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.all_eq_true_iff_forall_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p a (Std.DHashMap.Const.get m a h) = true
-- Mathlib.CategoryTheory.Shift.Basic
/-- shifting a morphism `f` by `n` is obtained by the notation `f⟦n⟧'`  -/
CategoryTheory.«term_⟦_⟧'» : Lean.TrailingParserDescr
-- Aesop.Util.Basic
Aesop.withExceptionPrefix : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.MessageData → m α → m α
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- The support of a summation filter (its `lim inf`, considered as a filter of sets).  -/
SummationFilter.support : {β : Type u_2} → SummationFilter β → Set β
-- Mathlib.Combinatorics.Graph.Delete
/-- The subgraph of `G` induced by a set `X` of vertices.
The edges are the edges of `G` with both ends in `X`.
(`X` is not required to be a subset of `V(G)` for this definition to work,
even though this is the standard use case)  -/
Graph.induce : {α : Type u_1} → {β : Type u_2} → Graph α β → Set α → Graph α β
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.coe_id : ∀ (α : Type u_2) [inst : SupSet α], ⇑(sSupHom.id α) = id
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.leftUnitor_inv_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f'),
  (CategoryTheory.Bicategory.leftUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f').inv
        (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id x) (CategoryTheory.eqToHom ⋯)))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The associator isomorphism for binary products.  -/
CategoryTheory.Limits.prod.associator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] → (P Q R : C) → (P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.extendCoordChange_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H},
  (ModelWithCorners.extendCoordChange e e').symm = ModelWithCorners.extendCoordChange e' e
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyGED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α → α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, Std.ExtDHashMap.Const.insertMany m [(k, v)] = m.insert k v
-- Mathlib.Probability.Kernel.WithDensity
/-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0`, `withDensity κ f` is s-finite.  -/
ProbabilityTheory.Kernel.instIsSFiniteKernelWithDensityOfNNReal : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] (f : α → β → NNReal),
  ProbabilityTheory.IsSFiniteKernel (κ.withDensity fun a b => ↑(f a b))