mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.Primrec.Basic
Primrec.beq : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : DecidableEq α], Primrec₂ BEq.beq
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a),
  Order.isSuccLimitRecOn b isMin succ isSuccLimit =
    Order.isSuccPrelimitRecOn b succ fun a ha => if h : IsMin a then isMin a h else isSuccLimit a ⋯
-- Mathlib.Algebra.CharP.IntermediateField
IntermediateField.charP' : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  (p : ℕ) [CharP E p], CharP (↥L) p
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBicone_whisker : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} {K : Type w₂} {g : K ≃ J}
  {f : J → C} (c : CategoryTheory.Limits.Bicone f), F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g
-- Mathlib.GroupTheory.ResiduallyFinite
Group.ResiduallyFinite.mk : ∀ {G : Type u_1} [inst : Group G], ⨅ H, H.toSubgroup = ⊥ → Group.ResiduallyFinite G
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.tensorHom_app_fst : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  {F₁ F₁' F₂ F₂' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorHom f g).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁'.obj j) (F₂'.obj j)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j))
      (f.app j)
-- Mathlib.Tactic.Push
/-- `push c` rewrites the goal by pushing the constant `c` deeper into an expression.
For instance, `push _ ∈ _` rewrites `x ∈ {y} ∪ zᶜ` into `x = y ∨ ¬ x ∈ z`.
More precisely, the `push` tactic repeatedly rewrites an expression by applying lemmas
of the form `c ... = ... (c ...)` (where `c` can appear 0 or more times on the right hand side).
To extend the `push` tactic, you can tag a lemma of this form with the `@[push]` attribute.

To instead move a constant closer to the head of the expression, use the `pull` tactic.

`push` works as both a tactic and a conv tactic.

* `push _ ~ _` pushes the (binary) operator `~`, `push ~ _` pushes the (unary) operator `~`.
* `push c at l1 l2 ...` rewrites at the given locations.
* `push c at *` rewrites at all hypotheses and the goal.
* `push +distrib Not` rewrites `¬ (p ∧ q)` into `¬ p ∨ ¬ q` (without `+distrib`, it rewrites it
  into `p → ¬ q` instead).
* `push (disch := tac) c` uses the tactic `tac` to discharge any hypotheses for `@[push]` lemmas.

Examples:
* `push Not` is the same as `push ¬ _`, and it rewrites `¬ ∀ ε > 0, ∃ δ > 0, δ < ε` into
  `∃ ε > 0, ∀ δ > 0, ε ≤ δ`. Notably, this preserves the binder names.
* `push _ ∈ _` rewrites `x ∈ {y} ∪ zᶜ` into `x = y ∨ ¬ x ∈ z`.
* `push (disch := positivity) Real.log` rewrites `log (a * b ^ 2)` into `log a + 2 * log b`.
* `push fun _ ↦ _` rewrites `fun x => f x ^ 2 + 5` into `f ^ 2 + 5`
* `push ∀ _, _` rewrites `∀ a, p a ∧ q a` into `(∀ a, p a) ∧ (∀ a, q a)`.
 -/
Mathlib.Tactic.Push.convPush_____ : Lean.ParserDescr
-- Init.Internal.Order.Lemmas
Lean.Order.Option.monotone_bindM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] {α β : Type u}
  {γ : Type w} [inst_2 : Lean.Order.PartialOrder γ] (f : γ → α → m (Option β)) (xs : Option α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Option.bindM (f x) xs
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.smul_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_3} {M : Type u_5}
  [inst_2 : TopologicalSpace M] [inst_3 : SMul R M] [inst_4 : ContinuousConstSMul R M] (r : R) (f : C(β, M))
  (g : C(α, β)), (r • f).comp g = r • f.comp g
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.ihom_coev_app : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F G : CategoryTheory.Functor D C), (CategoryTheory.ihom.coev F).app G = F.closedUnit.app G
-- Mathlib.Order.Filter.Cofinite
Filter.frequently_cofinite_mem_iff_infinite : ∀ {α : Type u_2} {s : Set α}, (∃ᶠ (x : α) in Filter.cofinite, x ∈ s) ↔ s.Infinite
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.pullback_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {Y X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X)
  (I : ((J.pullback f).obj S).Arrow),
  ↑(x.pullback f) I = ↑x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.exists_eq_tmul_of_forall : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  (∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n) → ∃ m n, x = m ⊗ₜ[R] n
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The inclusion from the locally discrete bicategory on the path category into the free bicategory
as a prelax functor. This will be promoted to a pseudofunctor after proving the coherence theorem.
See `inclusion`.
 -/
CategoryTheory.FreeBicategory.preinclusion : (B : Type u) →
  [inst : Quiver B] →
    CategoryTheory.PrelaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B))
      (CategoryTheory.FreeBicategory B)
-- Lean.Elab.Tactic.Calc
/-- Elaborator for the `calc` tactic mode variant.  -/
Lean.Elab.Tactic.evalCalc : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_pow : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (f : M₁ →L[R₁] M₁) (n : ℕ), ↑(f ^ n) = ↑f ^ n
-- Mathlib.LinearAlgebra.Prod
Submodule.snd_map_snd : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.map (LinearMap.snd R M M₂) (Submodule.snd R M M₂) = ⊤
-- Mathlib.Topology.Category.TopCat.Opens
/-- An open embedding `f : X ⟶ Y` induces a functor `Opens X ⥤ Opens Y`.
We define `IsOpenEmbedding.functor` as `IsOpenEmbedding.isOpenMap.functor`, so it won't
default to `IsInducing.functor` (which is equal but not defeq).
 -/
Topology.IsOpenEmbedding.functor : {X Y : TopCat} →
  {f : X ⟶ Y} →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
      CategoryTheory.Functor (TopologicalSpace.Opens ↑X) (TopologicalSpace.Opens ↑Y)
-- Mathlib.Topology.Compactness.LocallyCompact
/-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces,
`K : set X` is a compact set, and `U` is an open neighbourhood of `f '' K`,
then there exists a compact neighbourhood `L` of `K` such that `f` maps `L` to `U`.

This is a generalization of `exists_mem_nhds_isCompact_mapsTo`.  -/
exists_mem_nhdsSet_isCompact_mapsTo : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactPair X Y]
  {f : X → Y} {K : Set X} {U : Set Y},
  Continuous f → IsCompact K → IsOpen U → Set.MapsTo f K U → ∃ L ∈ nhdsSet K, IsCompact L ∧ Set.MapsTo f L U
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_div_two_pow : ∀ {a b n : ℕ}, (a &&& b) / 2 ^ n = a / 2 ^ n &&& b / 2 ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Auxiliary lemma for `biprod.uniqueUpToIso`.  -/
CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y}
  (hb : b.IsBilimit),
  (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).inv =
    CategoryTheory.Limits.biprod.desc b.inl b.inr
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of collinear points is finite-dimensional.  -/
Collinear.finiteDimensional_direction_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, Collinear k s → FiniteDimensional k ↥(affineSpan k s).direction
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.isSymm : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] {A : Matrix n n α}, A.IsDiag → A.IsSymm
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap_jacobian : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (h : Function.Bijective ⇑(algebraMap R S)), (Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap h).jacobian = 1
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_last_apply : ∀ {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n), (finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : Monoid M],
  MonoidAlgebra.ring =
    { toSemiring := MonoidAlgebra.semiring, toNeg := MonoidAlgebra.addCommGroup.toNeg,
      toSub := MonoidAlgebra.addCommGroup.toSub, toZSMul := MonoidAlgebra.addCommGroup.toZSMul, sub_eq_add_neg := ⋯,
      zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯,
      toIntCast := MonoidAlgebra.nonAssocRing.toAddCommGroupWithOne.toAddGroupWithOne.toIntCast, intCast_ofNat := ⋯,
      intCast_negSucc := ⋯ }
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  (X : AlgebraicGeometry.PresheafedSpace C) (x : ↑↑X),
  AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x =
    CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instRing : {σ : Type u_1} → {R : Type u_2} → [Ring R] → Ring (MvPowerSeries σ R)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.instSubsemiringClass : ∀ {R : Type u} [inst : NonAssocSemiring R], SubsemiringClass (Subsemiring R) R
-- Mathlib.Algebra.Polynomial.Lifts
/-- The polynomial `X` lifts.  -/
Polynomial.X_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S), Polynomial.X ∈ Polynomial.lifts f
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- `Ι a b` denotes the open-closed interval with unordered bounds. Here, `Ι` is a capital iota,
distinguished from a capital `i`.  -/
Interval.termΙ : Lean.ParserDescr
-- Mathlib.Topology.Order.Basic
nhdsLE_eq_iInf_principal : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderTopology α] {a : α},
  (∃ u, u < a) → nhdsWithin a (Set.Iic a) = ⨅ u, ⨅ (_ : u < a), Filter.principal (Set.Ioc u a)
-- Mathlib.Algebra.Group.WithOne.Basic
/-- Given an additive map from `α → β` returns an additive monoid homomorphism from
`WithZero α` to `WithZero β`  -/
WithZero.mapAddHom : {α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : Add β] → (α →ₙ+ β) → WithZero α →+ WithZero β
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.of_equivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (e : J ≌ J') [P.IsClosedUnderLimitsOfShape J], P.IsClosedUnderLimitsOfShape J'
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hexagon_reverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X Y Z : CategoryTheory.Arrow C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
        (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding Y Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X Z).hom Y))
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerSemicontinuousWithinAt_iff_frequently`. -/
LowerSemicontinuousWithinAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α} {s : Set α},
  (∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≤ y) → f x ≤ y) → LowerSemicontinuousWithinAt f s x
-- Mathlib.Data.Finsupp.Single
Finsupp.update_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) (i : α) [inst_1 : DecidableEq α],
  (f.update a b) i = if i = a then b else f i
-- Mathlib.Topology.ContinuousMap.Basic
/-- Given two continuous maps `f` and `g`, this is the continuous map `(x, y) ↦ (f x, g y)`.  -/
ContinuousMap.prodMap : {α₁ : Type u_5} →
  {α₂ : Type u_6} →
    {β₁ : Type u_7} →
      {β₂ : Type u_8} →
        [inst : TopologicalSpace α₁] →
          [inst_1 : TopologicalSpace α₂] →
            [inst_2 : TopologicalSpace β₁] →
              [inst_3 : TopologicalSpace β₂] → C(α₁, α₂) → C(β₁, β₂) → C(α₁ × β₁, α₂ × β₂)
-- Mathlib.Data.Ordmap.Ordnode
BinaryTree.toOrdNode.eq_2 : ∀ {α : Type u_1} (x_1 : α) (l r : BinaryTree α), (BinaryTree.node x_1 l r).toOrdNode = l.toOrdNode.node' x_1 r.toOrdNode
-- Mathlib.CategoryTheory.HomCongr
/-- If `X₁` is isomorphic to `X₂`, then there is a bijection between `X₁ ≅ Y` and `X₂ ≅ Y`.  -/
CategoryTheory.Iso.isoCongrLeft : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X₁ X₂ Y : C} → (X₁ ≅ X₂) → (X₁ ≅ Y) ≃ (X₂ ≅ Y)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_def : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C}
  (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X₂)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ g)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instPreorder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → [Preorder β] → Preorder (α →ₘ[μ] β)
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedGroup : {E : Type u_2} → [SeminormedGroup E] → SeminormedGroup Eᵒᵈ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.noinlineAttr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_alterKey_eq_isEmpty_eraseKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  (Std.Internal.List.Const.alterKey k f l).isEmpty =
    ((Std.Internal.List.eraseKey k l).isEmpty && (f (Std.Internal.List.getValue? k l)).isNone)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.card_lt_of_card_biUnion_lt : ∀ {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β} {c : Cardinal.{u}},
  Cardinal.mk ↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c → ∀ (a : α) (ha : a ∈ s), Cardinal.mk ↑(t a ha) < c
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.id_apply : ∀ {M : Type v} {ι : Type u_1} [inst : AddCommMonoid M] [inst_1 : Unique ι] (x : DirectSum ι fun x => M),
  (DirectSum.id M ι) x = x default
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_one : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.trunc (n + 1)) 1 = 1
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.comp_single : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Polynomial R)
  (i : ℕ) (m : M), (PolynomialModule.comp p) (PolynomialModule.single R i m) = p ^ i • PolynomialModule.single R 0 m
-- Init.Data.String.Length
String.length_append : ∀ (s t : String), (s ++ t).length = s.length + t.length
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.eq_5 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n.succ with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_5 m n
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Rescale a multivariate power series, as a `MonoidHom` in the scaling parameters.  -/
MvPowerSeries.rescaleMonoidHom : {σ : Type u_1} → {R : Type u_9} → [inst : CommSemiring R] → (σ → R) →* MvPowerSeries σ R →+* MvPowerSeries σ R
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.maxEntry : {α : Type u} → {β : Type v} → (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.isEmpty = false → α × β
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- The generator we chose for the annihilating ideal is monic when the ideal is non-zero.  -/
Polynomial.monic_annIdealGenerator : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  Polynomial.annIdealGenerator 𝕜 a ≠ 0 → (Polynomial.annIdealGenerator 𝕜 a).Monic
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_one : ↑1 = 1
-- Mathlib.GroupTheory.OrderOfElement
addSubgroupOfIdempotent.eq_1 : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S + S = S),
  addSubgroupOfIdempotent S hS1 hS2 = { carrier := S, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The elements of the Hilbert basis `mFourierBasis` are the functions `mFourierLp 2`, i.e. the
monomials `mFourier n` on `UnitAddTorus d` considered as elements of `L²`.  -/
UnitAddTorus.coe_mFourierBasis : ∀ {d : Type u_1} [inst : Fintype d], ⇑UnitAddTorus.mFourierBasis = UnitAddTorus.mFourierLp 2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.append_left : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeAddGroup.Red.Step L₂ L₃ → FreeAddGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.joinpoint.sizeOf_spec : ∀ (name : Lean.Name) (params : Array (Lean.Elab.Term.Do.Var × Bool)) (body k : Lean.Elab.Term.Do.Code),
  sizeOf (Lean.Elab.Term.Do.Code.joinpoint name params body k) =
    1 + sizeOf name + sizeOf params + sizeOf body + sizeOf k
-- Init.Data.SInt.Basic
/-- The number of distinct values representable by `Int32`, that is, `2^32 = 4294967296`.  -/
Int32.size : ℕ
-- Mathlib.Topology.Connected.Basic
isPreconnected_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsPreconnected {x}
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- This wraps the predicate `P : TopCat → Prop` in a typeclass.  -/
CompHausLike.HasProp : (TopCat → Prop) → (X : Type u) → [TopologicalSpace X] → Prop
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing bitvector functions such as `shiftLeft` and `rotateRight`.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceShift : Lean.Name → ℕ → ({n : ℕ} → BitVec n → ℕ → BitVec n) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Init.Data.List.Count
List.count_replicate_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {n : ℕ}, List.count a (List.replicate n a) = n
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipPrefix?_slice_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → s.skipPrefix? pat = some s.startPos
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.isPrimitive_primPart : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R), p.primPart.IsPrimitive
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ} (h : D₁ ≤ D₂),
  CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h = D₂.isTerminal.lift ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.mk.sizeOf_spec : ∀ (c? c_ww? c_wl? c_wr? : Option Lean.Expr),
  sizeOf { c? := c?, c_ww? := c_ww?, c_wl? := c_wl?, c_wr? := c_wr? } =
    1 + sizeOf c? + sizeOf c_ww? + sizeOf c_wl? + sizeOf c_wr?
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.factorsThrough_one_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.FactorsThrough 1 ↔ χ = 1