mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.isOpen_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
-- Mathlib.NumberTheory.ModularForms.NormTrace
_private.Mathlib.NumberTheory.ModularForms.NormTrace.0.ModularForm.eq_const_of_weight_zero₀ : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] (f : ModularForm 𝒢 0),
  ∃ c, ⇑f = Function.const UpperHalfPlane c
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.of_toArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isHyperbolic_conj'_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R),
  ((↑g)⁻¹ * m * ↑g).IsHyperbolic ↔ m.IsHyperbolic
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_one_left : ∀ (n : ℕ), Nat.uniformBell 1 n = 1
-- Mathlib.RingTheory.Flat.Basic
/-- Tensor product of injective maps are injective under some flatness conditions.
Also see `TensorProduct.map_injective_of_flat_flat'` and
`TensorProduct.map_injective_of_flat_flat_of_isDomain` for different flatness conditions.  -/
TensorProduct.map_injective_of_flat_flat : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {P : Type u_4} {Q : Type u_5}
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid Q] [inst_8 : Module R Q] (f : P →ₗ[R] M)
  (g : Q →ₗ[R] N) [Module.Flat R M] [Module.Flat R Q],
  Function.Injective ⇑f → Function.Injective ⇑g → Function.Injective ⇑(TensorProduct.map f g)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedMetaM : {α : Type} → Inhabited (Lean.MetaM α)
-- Mathlib.Logic.Basic
mem_dite : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {p : Prop} [inst_1 : Decidable p] {a : α} {s : p → β}
  {t : ¬p → β}, (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.completeSpace : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [inst_1 : ∀ (n : ℕ), DiscreteTopology (E n)],
  CompleteSpace ((n : ℕ) → E n)
-- Lean.Elab.PreDefinition.FixedParams
/-- To determine which parameters in mutually recursive predefinitions are fixed, and how they
correspond to each other, we run an analysis that aggregates information in the `Info` data type.

Abstractly, this represents
* a set `varying` of `(funIdx × paramIdx)` pairs known to be varying, initially empty
* a directed graph whose nodes are `(funIdx × paramIdx)` pairs, initially empty

We find the largest set and graph that satisfies these rules:
* Every parameter has to be related to itself: `(funIdx, paramIdx) → (funIdx, paramIdx)`.
* whenever the function with index `caller` calls `callee` and the `argIdx`'s argument is reducibly
  defeq to `paramIdx`, then we have an edge `(caller, paramIdx) → (callee, argIdx)`.
* whenever the function with index `caller` calls `callee` and the `argIdx`'s argument is not reducibly
  defeq to any of the `caller`'s parameters, then `(callee, argIdx) ∈ varying`.
* If we have `(caller, paramIdx₁) → (callee, argIdx)` and `(caller, paramIdx₂) → (callee, argIdx)`
  with `paramIdx₁ ≠ paramIdx₂`, then `(callee, argIdx) ∈ varying`.
* The graph is transitive
* If we have `(caller, paramIdx) → (callee, argIdx)` and `(caller, paramIdx) ∈ varying`, then
  `(callee, argIdx) ∈ varying`
* If the type of `funIdx`’s parameter `paramIdx₂ depends on the `paramIdx₁` and
  `(funIdx, paramIdx₁) ∈ varying`, then `(funIdx, paramIdx₁) ∈ varying`
* For structural recursion: The target and all its indices are `varying`.
  (This is taking into account post-hoc, using `FixedParamPerms.erase`)

Under the assumption that the predefinitions indeed are mutually recursive, then the resulting graph,
restricted to the non-`varying` nodes, should partition into cliques that have one member from each
function. Every such clique becomes a fixed parameter.

 -/
Lean.Elab.FixedParams.Info : Type
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_map_mul_map_inv : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R), (↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.find?_eq_find?_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  {it : Std.Iter β} {f : β → Bool}, it.find? f = (it.toIterM.find? f).run
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_some_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp}, t.find? x = some y → x ∈ t
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.mem_fixedPoints_iff_card_orbit_eq_one : ∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] {a : α}
  [inst_2 : Fintype ↑(AddAction.orbit M a)], a ∈ AddAction.fixedPoints M α ↔ Fintype.card ↑(AddAction.orbit M a) = 1
-- Mathlib.Order.Filter.Extr
IsMaxOn.inter : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → ∀ (t : Set α), IsMaxOn f (s ∩ t) a
-- Batteries.Data.Char.AsciiCasing
Char.toLower_toLower_eq_toLower : ∀ (c : Char), c.toLower.toLower = c.toLower
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.getCompletionKindForDecl : Lean.ConstantInfo → Lean.MetaM Lean.Lsp.CompletionItemKind
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.toBuilderName? : Aesop.Frontend.DBuilderName → Option Aesop.BuilderName
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- If a subgroup is generated by transpositions, then a transposition `swap x y` lies in the
subgroup if and only if `x` lies in the same orbit as `y`.  -/
swap_mem_closure_isSwap : ∀ {α : Type u_2} [inst : DecidableEq α] {S : Set (Equiv.Perm α)},
  (∀ f ∈ S, f.IsSwap) → ∀ {x y : α}, Equiv.swap x y ∈ Subgroup.closure S ↔ x ∈ MulAction.orbit (↥(Subgroup.closure S)) y
-- Mathlib.Geometry.Euclidean.SignedDist
/-- The signed distance between `s` and a point, in the direction of the reference point `p`.
This is expected to be used when `p` does not lie in `s` (in the degenerate case where `p` lies
in `s`, this yields 0) and when the point at which the distance is evaluated lies in the affine
span of `s` and `p` (any component of the distance orthogonal to that span is disregarded).  -/
AffineSubspace.signedInfDist : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            (s : AffineSubspace ℝ P) → [Nonempty ↥s] → [s.direction.HasOrthogonalProjection] → P → P →ᴬ[ℝ] ℝ
-- Mathlib.Data.List.Sort
StrictAnti.sortedLT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictAnti f → ((List.map f l).SortedLT ↔ l.SortedGT)
-- Mathlib.Logic.Equiv.Set
/-- The composition of an updated function with an equiv on a subtype can be expressed as an
updated function.  -/
dite_comp_equiv_update : ∀ {α : Type u_1} {E : Type u_2} {β : Sort u_3} {γ : Sort u_4} {p : α → Prop} [inst : EquivLike E { x // p x } β] (e : E)
  (v : β → γ) (w : α → γ) (j : β) (x : γ) [inst_1 : DecidableEq β] [inst_2 : DecidableEq α]
  [inst_3 : (j : α) → Decidable (p j)],
  (fun i => if h : p i then Function.update v j x (e ⟨i, h⟩) else w i) =
    Function.update (fun i => if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcCallParams.toJson : Lean.Lsp.RpcCallParams → Lean.Json
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.isEqvAux.match_1.splitter : {α : Type u_1} →
  (xs : Array α) →
    (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) →
      (x : ℕ) →
        (x_1 : x ≤ xs.size) →
          ((x : 0 ≤ xs.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h) → motive x x_1
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prevn.induct_unfolding : ∀ {s : String.Slice} (motive : s.Pos → ℕ → s.Pos → Prop),
  (∀ (p : s.Pos), motive p 0 p) →
    (∀ (p : s.Pos) (n : ℕ) (h : p ≠ s.startPos),
        motive (p.prev h) n ((p.prev h).prevn n) → motive p n.succ ((p.prev h).prevn n)) →
      (∀ (p : s.Pos) (n : ℕ), ¬p ≠ s.startPos → motive p n.succ p) → ∀ (p : s.Pos) (n : ℕ), motive p n (p.prevn n)
-- Init.PropLemmas
forall_eq_apply_imp_iff : ∀ {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : β → Prop}, (∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- The map `(X → M) → (Y → M)` induced by a map `X → Y` between finite types.  -/
FunOnFinite.map : {M : Type u_5} →
  [AddCommMonoid M] → {X : Type u_6} → {Y : Type u_7} → [Finite X] → [Finite Y] → (X → Y) → (X → M) → Y → M
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.eq_2 : ∀ (s a : String.Slice) (as : List String.Slice), s.intercalate (a :: as) = String.Slice.intercalate.go✝ a.copy s as
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddZeroClass : {α : Type u_1} → [AddZeroClass α] → AddZeroClass αᵐᵒᵖ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- `prod f g` is the product of `g a (f a)` over the support of `f`.  -/
Finsupp.prod : {α : Type u_1} → {M : Type u_8} → {N : Type u_10} → [inst : Zero M] → [CommMonoid N] → (α →₀ M) → (α → M → N) → N
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instFullIndFunctorOppositeTypeInclusion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Ind.inclusion C).Full
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instInhabitedGrindTacticM : {α : Type} → Inhabited (Lean.Elab.Tactic.Grind.GrindTacticM α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.mk.sizeOf_spec : ∀ (startLine endLine : ℕ) (kind? : Option Lean.Lsp.FoldingRangeKind),
  sizeOf { startLine := startLine, endLine := endLine, kind? := kind? } =
    1 + sizeOf startLine + sizeOf endLine + sizeOf kind?
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.foldrM_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  t₁.Equiv t₂ → Std.TreeSet.foldrM f init t₁ = Std.TreeSet.foldrM f init t₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.mk : Float → Float → Float → Float → Lean.Lsp.Color
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.degree f = 0 ↔ f.totalDegree = 0
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasFiniteProducts C}
  {inst_2 : CategoryTheory.Limits.HasPullbacks C} {X Y : CategoryTheory.Dial C} {x y : X.Hom Y},
  x.f = y.f → x.F = y.F → x = y
-- Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
_private.Mathlib.CategoryTheory.Limits.Indization.FilteredColimits.0.CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.term𝒢 : Lean.ParserDescr
-- Std.Async.System
/-- All the environment variables.
 -/
Std.Async.System.Environment : Type
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.issues : Lean.Meta.Grind.Result → List Lean.MessageData
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_uIoo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.uIoo i j = Set.uIoo (Fin.natAdd m i) (Fin.natAdd m j)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_alter_of_beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (k == k') = true → (k' ∈ Std.DHashMap.Raw.Const.alter m k f ↔ (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true)
-- Batteries.Data.List.Basic
List.sublists_eq_sublistsFast : @List.sublists = @List.sublistsFast
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.toList.isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Groupoid
/-- A Prop-valued typeclass asserting that a given category is a groupoid.  -/
CategoryTheory.IsGroupoid : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.mk : Lean.Meta.Grind.CasesTypes →
  Lean.Meta.Grind.ExtTheorems →
    Lean.NameSet →
      Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem →
        Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem → Lean.Meta.Grind.ExtensionState
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y) Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
        h)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mul_X_add_natCast_comp : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ}, (p * (Polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mk.inj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} X} {fst : CategoryTheory.Functor X A} {snd : CategoryTheory.Functor X C}
  {iso : fst.comp F ≅ snd.comp G} {fst_1 : CategoryTheory.Functor X A} {snd_1 : CategoryTheory.Functor X C}
  {iso_1 : fst_1.comp F ≅ snd_1.comp G},
  { fst := fst, snd := snd, iso := iso } = { fst := fst_1, snd := snd_1, iso := iso_1 } →
    fst = fst_1 ∧ snd = snd_1 ∧ iso ≍ iso_1
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  (CategoryTheory.MorphismProperty.isomorphisms D).inverseImage L = P.isoModSerre
-- Std.Time.Zoned.ZoneRules
/-- Local time that is not necessarily UTC.
 -/
Std.Time.TimeZone.UTLocal.local : Std.Time.TimeZone.UTLocal
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The torsion subgroup of the group of units.  -/
NumberField.Units.torsion : (K : Type u_1) → [inst : Field K] → Subgroup (NumberField.RingOfIntegers K)ˣ
-- Mathlib.Topology.UniformSpace.Defs
uniformContinuousOn_univ : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuousOn f Set.univ ↔ UniformContinuous f
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_iff_hasNoetherianRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {u v : V →ₗ[K] V₂}, u ≈ v ↔ (u - v).HasNoetherianRange
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.replaceHead_head : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (x : M i) (hnotone : x ≠ 1)
  (w : Monoid.CoprodI.NeWord M i j), (Monoid.CoprodI.NeWord.replaceHead x hnotone w).head = x
-- Lean.Data.Lsp.Basic
/-- Depending on the client capability
`workspace.workspaceEdit.resourceOperations` document changes are either
an array of `TextDocumentEdit`s to express changes to n different text
documents where each text document edit addresses a specific version of
a text document. Or it can contain above `TextDocumentEdit`s mixed with
create, rename and delete file / folder operations.

Whether a client supports versioned document edits is expressed via
`workspace.workspaceEdit.documentChanges` client capability.

If a client neither supports `documentChanges` nor
`workspace.workspaceEdit.resourceOperations` then only plain `TextEdit`s
using the `changes` property are supported.  -/
Lean.Lsp.WorkspaceEdit.documentChanges? : Lean.Lsp.WorkspaceEdit → Option (Array Lean.Lsp.DocumentChange)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection of `y` on `U` minimizes the distance `‖y - x‖` for `x ∈ U`.  -/
Submodule.starProjection_minimal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] (y : E), ‖y - U.starProjection y‖ = ⨅ x, ‖y - ↑x‖
-- Mathlib.SetTheory.Lists
Lists'.mem_def : ∀ {α : Type u_1} {b : Bool} {a : Lists α} {l : Lists' α b}, a ∈ l ↔ ∃ a' ∈ l.toList, a.Equiv a'
-- Mathlib.RingTheory.WittVector.Defs
/-- `WittVector p R` is the ring of `p`-typical Witt vectors over the commutative ring `R`,
where `p` is a prime number.

If `p` is invertible in `R`, this ring is isomorphic to `ℕ → R` (the product of `ℕ` copies of `R`).
If `R` is a ring of characteristic `p`, then `WittVector p R` is a ring of characteristic `0`.
The canonical example is `WittVector p (ZMod p)`,
which is isomorphic to the `p`-adic integers `ℤ_[p]`.  -/
WittVector : ℕ → Type u_1 → Type u_1
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_neg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), |(-a)| = |a|
-- Lean.Meta.Tactic.Grind.EMatch
/-- Matches offset pattern `pat+k` with term `e`  -/
Lean.Meta.Grind.EMatch.Cnstr.offset : Option Lean.Meta.Grind.GenPatternInfo → Lean.Expr → ℕ → Lean.Expr → Lean.Meta.Grind.EMatch.Cnstr
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withIncDischargeDepth : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Data.Set.Restrict
Set.range_extend_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ),
  Set.range (Function.extend f g g') ⊆ Set.range g ∪ g' '' (Set.range f)ᶜ
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.mk : {α : Type u} → α → CategoryTheory.Codiscrete α
-- Mathlib.Order.Filter.Finite
Filter.frequently_exists_finite : ∀ {α : Type u} {ι : Type u_2} {I : Set ι},
  I.Finite → ∀ {l : Filter α} {p : ι → α → Prop}, (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofInt : ∀ {n : ℤ}, (Int64.ofInt n).toInt16 = Int16.ofInt n
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- `∣` is not a useful definition if an inverse is available.  -/
GroupWithZero.dvd_iff : ∀ {α : Type u_1} [inst : GroupWithZero α] {m n : α}, m ∣ n ↔ m = 0 → n = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Mathlib.Analysis.InnerProductSpace.MeanErgodic
_private.Mathlib.Analysis.InnerProductSpace.MeanErgodic.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_exs : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}
  {v : α → M}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- A shorthand to bundle the μₗ as an isomorphism  -/
CategoryTheory.Functor.LeftLinear.μₗIso : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        (F : CategoryTheory.Functor D D') →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] →
                    [F.LeftLinear C] →
                      (c : C) →
                        (d : D) →
                          CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ≅
                            F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
-- Mathlib.Algebra.Group.Subgroup.Finsupp
Subgroup.mem_closure_range_iff : ∀ {M : Type u_1} [inst : CommGroup M] {ι : Type u_2} {f : ι → M} {x : M},
  x ∈ Subgroup.closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
_private.Mathlib.RingTheory.Perfectoid.FontaineTheta.0.term𝔭 : Lean.ParserDescr
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_cancel_right : ∀ {α : Type u_1} {s t : Set α}, s ∩ t ⊆ ∅ → (s ∪ t) \ t = s
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.termSum.eq_1 : ∀ (s : ℝ) (N : ℕ), ZetaAsymptotics.termSum s N = ∑ n ∈ Finset.range N, ZetaAsymptotics.term (n + 1) s
-- Init.Data.Int.Order
Int.max_comm : ∀ (a b : ℤ), max a b = max b a
-- Mathlib.Algebra.Ring.SumsOfSquares
Subsemiring.sumSq_toNonUnitalSubsemiring : ∀ {T : Type u_2} [inst : CommSemiring T], (Subsemiring.sumSq T).toNonUnitalSubsemiring = NonUnitalSubsemiring.sumSq T
-- Mathlib.Data.List.Map2
List.zipRight_nil_right : ∀ {α : Type u} {β : Type v} (as : List α), as.zipRight [] = []
-- Mathlib.RingTheory.Jacobson.Ring
/-- A ring is a Jacobson ring if for every radical ideal `I`,
the Jacobson radical of `I` is equal to `I`.
See `isJacobsonRing_iff_prime_eq` and `isJacobsonRing_iff_sInf_maximal`
for equivalent definitions.  -/
IsJacobsonRing : (R : Type u_3) → [CommRing R] → Prop
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_smul_const : ∀ {σ : Type u_4} {R : Type u_5} [inst : CommSemiring R] (e : σ →₀ ℕ) (r : R),
  (MvPowerSeries.monomial e) (r ^ e.sum fun x n => n) = e.prod fun s e => (r • MvPowerSeries.X s) ^ e
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- If `I ≤ J`, then every tagged prepartition of `I` is a tagged prepartition of `J`.  -/
BoxIntegral.TaggedPrepartition.embedBox : {ι : Type u_1} → (I J : BoxIntegral.Box ι) → I ≤ J → BoxIntegral.TaggedPrepartition I ↪ BoxIntegral.TaggedPrepartition J
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.codisjoint_addSubgroupOf_sup : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G),
  Codisjoint (H.addSubgroupOf (H ⊔ K)) (K.addSubgroupOf (H ⊔ K))
-- Mathlib.Topology.EMetricSpace.Defs
edist_congr_left : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y z : α}, edist x y = 0 → edist z x = edist z y