mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`y, z ∈ S`, we have `(f y)⁻¹ = (f z)⁻¹ → f y = f z`.  -/
Submonoid.LocalizationMap.inv_inj : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (hf : ∀ (y : ↥S), IsUnit (f ↑y)) {y z : ↥S},
  ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹ → f ↑y = f ↑z
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The graph isomorphism between the top element of `G.subgraph` and `G`.  -/
SimpleGraph.Subgraph.topIso : {V : Type u} → {G : SimpleGraph V} → ⊤.coe ≃g G
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_C_mul_X : ∀ {R : Type u} [inst : Semiring R] (x : R) (n : ℕ), (Polynomial.C x * Polynomial.X).coeff n = if n = 1 then x else 0
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_zero : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ↑0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (x : G.obj a),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a)) (Sum.inr x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coprod.inr.app a)) x
-- Mathlib.Algebra.Algebra.Defs
/-- This has high priority because it is almost always the right instance when it applies.  -/
IsScalarTower.right : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], IsScalarTower R A A
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.compactlyGeneratedToTop_obj : ∀ (self : CompactlyGenerated), CompactlyGenerated.compactlyGeneratedToTop.obj self = self.toTop
-- Mathlib.Data.Multiset.Count
Multiset.countP_cons_of_pos : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
  p a → Multiset.countP p (a ::ₘ s) = Multiset.countP p s + 1
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- Whiskering commutes with the enriched composition.  -/
CategoryTheory.eComp_eHomWhiskerRight_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' : C}
  (f : X ⟶ X') (Y Z : C) {Z_1 : V} (h : (X ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X' Y Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f Z) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerRight V f Y) (Y ⟶[V] Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_map_subset : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  (x : HahnSeries Γ R) (f : ZeroHom R S), (x.map f).support ⊆ x.support
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂)[k] = t₁[k]
-- Mathlib.Data.List.Pairwise
List.pairwise_cons_cons_iff_of_trans : ∀ {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} {a b : α},
  List.Pairwise R (a :: b :: l) ↔ R a b ∧ List.Pairwise R (b :: l)
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_const_mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜'), a ≠ 0 → logDeriv (fun z => a * f z) x = logDeriv f x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (F.map f) (app b) ≅
                      CategoryTheory.CategoryStruct.comp (app a) (G.map f)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b))
                        (naturality g).hom =
                      CategoryTheory.CategoryStruct.comp (naturality f).hom
                        (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
                  CategoryTheory.Oplax.StrongTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a)).hom
                          (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a)) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
                            (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
                    CategoryTheory.Oplax.StrongTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g)).hom
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
                                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
                      CategoryTheory.Oplax.StrongTrans.naturality_comp._autoParam →
                    CategoryTheory.Oplax.StrongTrans F G
-- Mathlib.Analysis.Convex.Topology
/-- If `s` is a convex set, then `a • s + b • interior s ⊆ interior s` for all `0 ≤ a`, `0 < b`,
`a + b = 1`. See also `Convex.combo_closure_interior_subset_interior` for a stronger version.  -/
Convex.combo_self_interior_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {a b : 𝕜}, 0 ≤ a → 0 < b → a + b = 1 → a • s + b • interior s ⊆ interior s
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult.mk.injEq : ∀ (capabilities : Lean.Lsp.ServerCapabilities) (serverInfo? : Option Lean.Lsp.ServerInfo)
  (capabilities_1 : Lean.Lsp.ServerCapabilities) (serverInfo?_1 : Option Lean.Lsp.ServerInfo),
  ({ capabilities := capabilities, serverInfo? := serverInfo? } =
      { capabilities := capabilities_1, serverInfo? := serverInfo?_1 }) =
    (capabilities = capabilities_1 ∧ serverInfo? = serverInfo?_1)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.adapt_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε ε' α : Type u}
  (f : ε → ε') (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε' → Pred) EPred),
  ⦃ Std.Internal.Do.wp x post (EPost.Cons.mk✝ (fun e => epost.head (f e)) epost.tail) ⦄ ExceptT.adapt f x ⦃ post;
    epost ⦄
-- Init.Meta.Defs
Lean.Syntax.isFieldIdx? : Lean.Syntax → Option ℕ
-- Mathlib.RingTheory.LocalProperties.Exactness
exact_of_localized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid L]
  [inst_6 : Module R L] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (f : M →ₗ[R] N) (g : N →ₗ[R] L),
      (∀ (r : ↑s),
          Function.Exact ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)
            ⇑((LocalizedModule.map (Submonoid.powers ↑r)) g)) →
        Function.Exact ⇑f ⇑g
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivWithinAt.continuousAlternatingMap_apply_const : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  {c' : E →L[𝕜] F [⋀^ι]→L[𝕜] G} [inst_7 : Fintype ι],
  HasFDerivWithinAt c c' s x → ∀ (u : ι → F), HasFDerivWithinAt (fun x => (c x) u) (c'.flipAlternating u) s x
-- Mathlib.Algebra.Group.Hom.Defs
/-- The inverse of a bijective `AddMonoidHom` is an `AddMonoidHom`.  -/
AddMonoidHom.inverse : {A : Type u_10} →
  {B : Type u_11} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        (f : A →+ B) → (g : B → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B →+ A
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The functor `toKaroubi C : C ⥤ Karoubi C` is fully faithful.  -/
CategoryTheory.Idempotents.fullyFaithfulToKaroubi : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → (CategoryTheory.Idempotents.toKaroubi C).FullyFaithful
-- Mathlib.Order.OrderDual
OrderDual.ext : ∀ {α : Type u_1} {a b : αᵒᵈ}, OrderDual.ofDual a = OrderDual.ofDual b → a = b
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.id_reflectsColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeMapCoconeInv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D}
  (H : CategoryTheory.Functor D C) [inst_3 : H.IsEquivalence] (c : CategoryTheory.Limits.Cocone (F.comp H)),
  CategoryTheory.Functor.mapCoconeMapCoconeInv H c =
    (CategoryTheory.Limits.Cocone.functorialityEquivalence F H.asEquivalence).counitIso.app c
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n')
  (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q),
  (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow •
      CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' ⋯).hom (γ.v p' q hp')
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.instInhabitedNormedSpaceInfo.default : Manifold.Elab.NormedSpaceInfo
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.isUniformInducing_extension : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [CompleteSpace β],
  IsUniformInducing f → IsUniformInducing (UniformSpace.Completion.extension f)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_zsmul : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddGroup (G i)] [inst_3 : ∀ (i : ι), AddSubgroupClass (S i) (G i)]
  (i : ι) (r : G i) (n : ℤ), RestrictedProduct.single A i (n • r) = n • RestrictedProduct.single A i r
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.prodPrimes_squarefree : ∀ (self : BoundingSieve), Squarefree self.prodPrimes
-- Init.Data.Nat.ToString
Nat.five_eq_digitChar : ∀ {n : ℕ}, '5' = n.digitChar ↔ n = 5
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms.0.SimplexCategoryGenRel.simplicialInsert.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (b : ℕ) (l : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (b : ℕ) → (l : List ℕ) → motive (b :: l)),
  (match b :: l with
    | [] => h_1 ()
    | b :: l => h_2 b l) =
    h_2 b l
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.instZero : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → [Nontrivial R] → Zero ↑(Set.Ico 0 1)
-- Lean.Data.Lsp.Internal
/-- Start character of the range of this location.  -/
Lean.Lsp.RefInfo.Location.startPosCharacter : Lean.Lsp.RefInfo.Location → ℕ
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_sdiff_Ioc : ∀ {α : Type u_2} {a b : α} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : LocallyFiniteOrderBot α],
  Finset.Iic b \ Finset.Ioc a b = Finset.Iic (min a b)
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_mulVec : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α)
  (x : l ⊕ m → α),
  (Matrix.fromBlocks A B C D).mulVec x =
    Sum.elim (A.mulVec (x ∘ Sum.inl) + B.mulVec (x ∘ Sum.inr)) (C.mulVec (x ∘ Sum.inl) + D.mulVec (x ∘ Sum.inr))
-- Mathlib.Order.Minimal
minimal_le_iff : ∀ {α : Type u_2} {x y : α} [inst : Preorder α], Minimal (fun x => x ≤ y) x ↔ x ≤ y ∧ IsMin x
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sup : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l l' : Filter α}, f =O[l] g' → f =O[l'] g' → f =O[l ⊔ l'] g'
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
inhomogeneousCochains.d.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Monoid G] (A : Rep.{u_1, u, u} k G) (n : ℕ),
  inhomogeneousCochains.d A n =
    ModuleCat.ofHom
      {
        toFun := fun f g =>
          (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 => x1 * x2) g),
        map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The inclusion of a SubMulAction into the ambient set, as an equivariant map  -/
SubMulAction.inclusion : {M : Type u_1} → {α : Type u_2} → [inst : Monoid M] → [inst_1 : MulAction M α] → (s : SubMulAction M α) → ↥s →ₑ[id] α
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure_iUnion : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_3} (s : ι → Set M),
  Subsemigroup.closure (⋃ i, s i) = ⨆ i, Subsemigroup.closure (s i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.revAll_eq_true_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.revAll pat = true ↔ String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat s.startPos s.endPos
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.get : Lean.Meta.FVarSubst → Lean.FVarId → Lean.Expr
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
HomologicalComplex.shortComplexTruncLE.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K K_1 : HomologicalComplex C c'),
  K = K_1 →
    ∀ (e e_1 : c.Embedding c') (e_e : e = e_1) [inst_2 : e.IsTruncLE],
      K.shortComplexTruncLE e = K_1.shortComplexTruncLE e_1
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.moment.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℕ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.moment X p μ = ∫ (x : Ω), (X ^ p) x ∂μ
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.priority : Lean.Parser.Category
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioc_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioc a b)), Subtype.val '' Set.Ioi c = Set.Ioc (↑c) b
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- `H¹(L_{S/R})`, the first homology of the (naive) cotangent complex of `S` over `R`.  -/
Algebra.H1Cotangent : (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max u v)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_add_right_singleton : ∀ {α : Type u_2} [inst : AddGroup α] {a b : α}, {b}.preimage (fun x => x + a) ⋯ = {b + -a}
-- Lean.Meta.Tactic.Grind.ForallProp
/-- Applies the following rewriting rules:
- `Grind.imp_true_eq`
- `Grind.imp_false_eq`
- `Grind.forall_imp_eq_or`
- `Grind.true_imp_eq`
- `Grind.false_imp_eq`
- `Grind.imp_self_eq`
- `forall_true`
- `forall_false`
- `Grind.forall_or_forall`
- `Grind.forall_forall_or`
- `Grind.forall_and`
 -/
Lean.Meta.Grind.simpForall : Lean.Meta.Simp.Simproc
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.orbitRelEquiv_apply_mk'' : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (w : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.orbitRelEquiv (Quotient.mk'' w) = w.comap (algebraMap k K)
-- Init.Data.SInt.Bitwise
Int16.or_zero : ∀ {a : Int16}, a ||| 0 = a
-- Lean.Parser.Syntax
Lean.Parser.Command.postfix.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.δ_one_eq_const : SSet.stdSimplex.δ 1 = SSet.const (SSet.stdSimplex.obj₀Equiv.symm 0)
-- Mathlib.RingTheory.Perfection
Perfection.lift_symm_apply : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [inst : CommSemiring R] [inst_1 : CharP R p]
  [inst_2 : PerfectRing R p] (S : Type u₂) [inst_3 : CommSemiring S] [inst_4 : CharP S p] (f : R →+* Perfection S p),
  (Perfection.lift p R S).symm f = (Perfection.coeff S p 0).comp f
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_unshift : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F), (p.unshift z).radius = p.radius
-- Mathlib.Order.WithBot
WithBot.toDual.eq_1 : ∀ {α : Type u_1}, WithBot.toDual = Equiv.refl (WithBot α)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α)
  (f f_1 : Option (β k) → Option (β k)),
  f = f_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.alter k f t hl = Std.DTreeMap.Internal.Impl.alter k f_1 t hl
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.length_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keys_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} (h : t.WF),
  (Std.TreeMap.Raw.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x t[x])
        t.keys.attach).unattach
-- Mathlib.Analysis.Convex.Body
/-- Let `K` be a convex body that contains `0` and let `u n` be a sequence of nonnegative real
numbers that tends to `0`. Then the intersection of the dilated bodies `(1 + u n) • K` is equal
to `K`.  -/
ConvexBody.iInter_smul_eq_self : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [T2Space V] {u : ℕ → NNReal}
  (K : ConvexBody V), 0 ∈ K → Filter.Tendsto u Filter.atTop (nhds 0) → ⋂ n, (1 + ↑(u n)) • ↑K = ↑K
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.withStackDrop : ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.ae_iff : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → ∀ {p : 𝓧 → Prop}, Measurable p → ((∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂μ, p x)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- Given a `n`-simplex of `X.op` that is constant on the boundary, this
is the corresponding `n`-simplex of `X`.  -/
SSet.PtSimplex.unop : {X : SSet} →
  {n : ℕ} → {x : X.obj (Opposite.op { len := 0 })} → X.op.PtSimplex n (SSet.opObjEquiv.symm x) → X.PtSimplex n x
-- Init.Data.UInt.Lemmas
UInt16.le_iff_lt_or_eq : ∀ {a b : UInt16}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Algebra.Order.Monoid.Defs
mul_self_lt_one_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a * a < 1 ↔ a < 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Γ_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ),
  AlgebraicGeometry.PresheafedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minKey?_of_isSome_minKey?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  (Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l)).isSome = true →
    (Std.Internal.List.minKey? l).isSome = true
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.Monic.roots_map_of_card_eq_natDegree : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {p : Polynomial A},
  p.Monic → ∀ (f : A →+* B), p.roots.card = p.natDegree → Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
-- Mathlib.Data.EReal.Basic
EReal.coe_neg' : ∀ {x : ℝ}, ↑x < 0 ↔ x < 0
-- Init.System.IO
/-- Whether the standard input, output, and error handles of a child process should be attached to
pipes, inherited from the parent, or null.

If the stream is a pipe, then the parent process can use it to communicate with the child.
 -/
IO.Process.Stdio : Type
-- Mathlib.Topology.Filter
Filter.nhds_bot : ∀ {α : Type u_2}, nhds ⊥ = pure ⊥