mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdjoinRoot
/-- `AdjoinRoot.map` as an `AlgHom`.  -/
AdjoinRoot.mapAlgHom : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                (f : S →ₐ[R] T) →
                  (p : Polynomial S) → (q : Polynomial T) → q ∣ Polynomial.map (↑f) p → AdjoinRoot p →ₐ[R] AdjoinRoot q
-- Mathlib.Topology.CompactOpen
ContinuousMap.eventually_range_subset : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {U : Set Y} [CompactSpace X]
  {f : C(X, Y)}, IsOpen U → Set.range ⇑f ⊆ U → ∀ᶠ (g : C(X, Y)) in nhds f, Set.range ⇑g ⊆ U
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.lift_mk_one : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (m : M),
  (LocalizedModule.lift S g h) (LocalizedModule.mk m 1) = g m
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.map_id_equiv : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp},
  (Std.TreeMap.Raw.map (fun x v => v) t).Equiv t
-- Mathlib.Data.ENNReal.Operations
ENNReal.not_lt_top : ∀ {x : ENNReal}, ¬x < ⊤ ↔ x = ⊤
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_mul_cancel_of_dvd : ∀ {a b : ℤ}, b ∣ a → a.tdiv b * b = a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.getEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} (c : Std.DTreeMap.Internal.Cell α β (compare k)),
  c.getEntry? =
    match c.inner with
    | none => none
    | some p => some ⟨p.fst, p.snd⟩
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntryD.eq_2 : ∀ {α : Type u} {β : Type v} (x : α × β) (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntryD
      (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x =
    (k, v)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Transfer `Coframe` across an `Equiv`.  -/
Equiv.coframe : {α : Type u} → {β : Type v} → α ≃ β → [Order.Coframe β] → Order.Coframe α
-- Mathlib.Data.Prod.Lex
Prod.Lex.instDenselyOrderedLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [DenselyOrdered α] [DenselyOrdered β],
  DenselyOrdered (Lex (α × β))
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Integral $\oint_{|z-c|=R} \frac{dz}{z-w} = 2πi$ whenever $|w-c| < R$.  -/
circleIntegral.integral_sub_inv_of_mem_ball : ∀ {c w : ℂ} {R : ℝ}, w ∈ Metric.ball c R → ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * ↑Real.pi * Complex.I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constAlter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ →
    ∀ (k : α) (f : Option β → Option β), (Std.DTreeMap.Const.alter t₁ k f).Equiv (Std.DTreeMap.Const.alter t₂ k f)
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.Functor.toReflPrefunctor.map_comp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E),
  (F.comp G).toReflPrefunctor = F.toReflPrefunctor ⋙rq G.toReflPrefunctor
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldr_eq_foldr_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : α → β → δ → δ} {init : δ},
  Std.DTreeMap.Raw.foldr f init t = List.foldr (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Raw.Const.toList t)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.go : {α : Type u_1} → [Lean.Grind.Ring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Poly → α → α
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.toArrayFn : {α σ : Type} → Lean.SimplePersistentEnvExtensionDescr α σ → List α → Array α
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.instDivisionRing : {α : Type u} → {β : Type v} → {φ : Ultrafilter α} → [DivisionRing β] → DivisionRing ((↑φ).Germ β)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- Given a type `C`, the free monoidal category over `C` has as objects formal expressions built from
(formal) tensor products of terms of `C` and a formal unit. Its morphisms are compositions and
tensor products of identities, unitors and associators.
 -/
CategoryTheory.FreeMonoidalCategory : Type u → Type u
-- Mathlib.Topology.Category.Stonean.Limits
Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier : CompHausLike.HasExplicitPullbacksOfInclusions fun Y => ExtremallyDisconnected ↑Y
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.

`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.

This function is deprecated. Instead of `it.ensureTermination.findM?`, use `it.findM?`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Std.Iter.Partial.findM? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id m] → Std.Iter.Partial β → (β → m (ULift.{w, 0} Bool)) → m (Option β)
-- Mathlib.Order.Fin.Basic
/-- The ordering on `Fin n` is a well order.  -/
Fin.Lt.isWellOrder : ∀ (n : ℕ), IsWellOrder (Fin n) fun x1 x2 => x1 < x2
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset_6 : HAdd Std.Time.WallTime Std.Time.Nanosecond.Offset Std.Time.WallTime
-- Lean.Parser.Basic
/-- The syntax stack height prior to the failing parser's execution  -/
Lean.Parser.RecoveryContext.initialSize : Lean.Parser.RecoveryContext → ℕ
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.tryTacticElabAttribute.unsafe_impl_2 : IO (Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Try.TryTactic)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.inv_μₗ : ∀ {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'] [inst_6 : F.LeftLinear C] (c : C) (d : D),
  CategoryTheory.inv (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d) = CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.instAddCommGroup : (A : Type uA) → [inst : AddCommGroup A] → AddCommGroup (CharacterModule A)
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.fromCols_replicateCol0_isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {n' : Type u_4} {R : Type u_5} [inst : CommRing R] (A : Matrix m n R),
  (A.fromCols (Matrix.replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_inter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂
-- Mathlib.Data.Option.Basic
Option.mem_map_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ {a : α} {o : Option α}, f a ∈ Option.map f o ↔ a ∈ o
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.mono_of_eq_fst_snd' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a : R ⟶ X},
  CategoryTheory.IsKernelPair f a a → CategoryTheory.Mono f
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_map_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {N₂ : Type u_6} [inst_7 : AddCommMonoid N₂] [inst_8 : Module R N₂] (f : M →ₗ[R] N₂ →ₗ[R] P)
  (g : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N),
  Submodule.map₂ f p (Submodule.map g q) = Submodule.map₂ (f.compl₂ g) p q
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- `MeasureTheory.Lp.compMeasurePreserving` as a linear map.  -/
MeasureTheory.Lp.compMeasurePreservingₗ : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] →
            {β : Type u_7} →
              [inst_1 : MeasurableSpace β] →
                {μb : MeasureTheory.Measure β} →
                  (𝕜 : Type u_8) →
                    [inst_2 : NormedRing 𝕜] →
                      [inst_3 : Module 𝕜 E] →
                        [inst_4 : IsBoundedSMul 𝕜 E] →
                          (f : α → β) →
                            MeasureTheory.MeasurePreserving f μ μb →
                              ↥(MeasureTheory.Lp E p μb) →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkipWhile_le_of_isLongestRevMatchAtChain : ∀ {ρ : 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} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos → endPos.revSkipWhile pat ≤ startPos
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₂.contains k = true → (m₁.diff m₂).get! k = default
-- Mathlib.CategoryTheory.Sites.Precoverage
_private.Mathlib.CategoryTheory.Sites.Precoverage.0.CategoryTheory.Precoverage.comp_mem_coverings.match_1_1.eq_1 : ∀ (ι' α : Type (max u_1 u_2)) (fib : ι' ⊕ α → Type (max u_1 u_2)) (motive : (i : ι' ⊕ α) → fib i → Sort u_3) (i : ι')
  (j : fib (Sum.inl i)) (h_1 : (i : ι') → (j : fib (Sum.inl i)) → motive (Sum.inl i) j)
  (h_2 : (i : α) → (j : fib (Sum.inr i)) → motive (Sum.inr i) j),
  (match Sum.inl i, j with
    | Sum.inl i, j => h_1 i j
    | Sum.inr i, j => h_2 i j) =
    h_1 i j
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_iff_forall_eq : ∀ {s : String.Slice}, s.isEmpty = true ↔ ∀ (p q : s.Pos), p = q
-- Init.Data.Dyadic.Basic
Dyadic.not_le : ∀ {x y : Dyadic}, ¬x < y ↔ y ≤ x
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.newEntries : {γ : Type} → Lean.KeyedDeclsAttribute.ExtensionState γ → List Lean.KeyedDeclsAttribute.OLeanEntry
-- Mathlib.Tactic.Linter.UnusedTacticExtension
/-- `Parser`s allowed to not change the tactic state.
This can be increased dynamically, using `#allow_unused_tactic`.
 -/
Mathlib.Linter.UnusedTactic.allowedRef : IO.Ref (Std.HashSet Lean.SyntaxNodeKind)
-- Mathlib.Algebra.Module.GradedModule
/-- A graded version of `Module`.  -/
DirectSum.Gmodule : {ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [VAdd ιA ιB] →
            [(i : ιA) → AddMonoid (A i)] →
              [(i : ιB) → AddMonoid (M i)] → [GradedMonoid.GMonoid A] → Type (max (max (max u_1 u_2) u_3) u_4)
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- The identity natural transformation exhibits a simplicial set as a right extension of its
restriction along `(Truncated.inclusion (n := n)).op`.  -/
SSet.Truncated.rightExtensionInclusion : (X : SSet) →
  (n : ℕ) →
    (SimplexCategory.Truncated.inclusion n).op.RightExtension ((SimplexCategory.Truncated.inclusion n).op.comp X)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] (toIsAdjoinRoot : IsAdjoinRoot S f) (monic : f.Monic),
  sizeOf { toIsAdjoinRoot := toIsAdjoinRoot, monic := monic } = 1 + sizeOf toIsAdjoinRoot + sizeOf monic
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.pow_map_zero_of_le : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : Module.End R M} {m : M} {k l : ℕ}, k ≤ l → (f ^ k) m = 0 → (f ^ l) m = 0
-- Mathlib.Order.Interval.Finset.Defs
Prod.instLocallyFiniteOrderTop.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] [inst_4 : DecidableLE (α × β)],
  Prod.instLocallyFiniteOrderTop = LocallyFiniteOrderTop.ofIci' (α × β) (fun x => Finset.Ici x.1 ×ˢ Finset.Ici x.2) ⋯
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.isUnit_C : ∀ {R : Type u} [inst : Semiring R] {x : R}, IsUnit (Polynomial.C x) ↔ IsUnit x
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedMonoid.mul_le_mul_right : ∀ {α : Type u_2} {inst : CommMonoid α} {inst_1 : Preorder α} [self : IsOrderedMonoid α] (a b : α),
  a ≤ b → ∀ (c : α), c * a ≤ c * b
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to an `Int8`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toInt8 : Float.Model.UnpackedFloat → Int8
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.mk.injEq : ∀ (root : Lean.TSyntax `tactic) (terminal : Bool) (config : Lean.Try.Config) (originalMaxHeartbeats : ℕ)
  (root_1 : Lean.TSyntax `tactic) (terminal_1 : Bool) (config_1 : Lean.Try.Config) (originalMaxHeartbeats_1 : ℕ),
  ({ root := root, terminal := terminal, config := config, originalMaxHeartbeats := originalMaxHeartbeats } =
      { root := root_1, terminal := terminal_1, config := config_1,
        originalMaxHeartbeats := originalMaxHeartbeats_1 }) =
    (root = root_1 ∧ terminal = terminal_1 ∧ config = config_1 ∧ originalMaxHeartbeats = originalMaxHeartbeats_1)
-- Mathlib.Data.UInt
UInt16.toBitVec_natCast : ∀ (n : ℕ), (↑n).toBitVec = ↑n
-- Lean.Message
Lean.MessageData.nestD : Lean.MessageData → Lean.MessageData
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.not_bddAbove_setOfPred_isPrincipal`.

---

Principal ordinals under any operation are unbounded.  -/
Ordinal.not_bddAbove_principal : ∀ (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}), ¬BddAbove {o | Ordinal.IsPrincipal op o}
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.pow_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ g i) → MonovaryOn f g s → ∀ (n : ℕ), MonovaryOn f (g ^ n) s
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.generateHas_def : ∀ {α : Type u_3} {C : Set (Set α)},
  (MeasurableSpace.DynkinSystem.generate C).Has = MeasurableSpace.DynkinSystem.GenerateHas C
-- Mathlib.Topology.Algebra.Order.Group
tendsto_one_iff_mabs_tendsto_one : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {α : Type u_2} {l : Filter α} (f : α → G),
  Filter.Tendsto f l (nhds 1) ↔ Filter.Tendsto (mabs ∘ f) l (nhds 1)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_id : ∀ {β : Type u_2} (N : Matroid β), N.comap id = N
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.eval_comp_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), AdicCompletion.eval I M n ∘ₗ AdicCompletion.of I M = (I ^ n • ⊤).mkQ
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toPartialHomeomorphOfImageEq.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e e_1 : X ≃ₜ Y)
  (e_e : e = e_1) (s s_1 : Set X) (e_s : s = s_1) (t t_1 : Set Y) (e_t : t = t_1) (h : ⇑e '' s = t),
  e.toPartialHomeomorphOfImageEq s t h = e_1.toPartialHomeomorphOfImageEq s_1 t_1 ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k fallback : α},
  (Std.ExtDHashMap.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (m.get x_2 ⋯)).isSome).getD fallback
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiRing_eq_iff : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : Fintype ι] {z₁ z₂ : M₂}, MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
-- Lean.Elab.PreDefinition.FixedParams
/-- If `type` is the type of the `funIdx`'s function, instantiate the fixed parameters.
 -/
Lean.Elab.FixedParamPerm.instantiateForall : Lean.Elab.FixedParamPerm → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Category.Profinite.Basic
CompHaus.toProfinite_obj' : ∀ (X : CompHaus), ↑(CompHaus.toProfinite.obj X).toTop = ConnectedComponents ↑X.toTop
-- Init.Data.Vector.Erase
Vector.eraseIdx_append_of_lt_size : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {k : ℕ} (hk : k < n) (xs' : Vector α m) (h : k < n + m),
  (xs ++ xs').eraseIdx k h = Vector.cast ⋯ (xs.eraseIdx k hk ++ xs')
-- Mathlib.Algebra.Notation.Defs
instHVAdd : {α : Type u_1} → {β : Type u_2} → [VAdd α β] → HVAdd α β β
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.finrank_lt_iff_rank_lt : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {n : ℕ}, Module.finrank K V < n ↔ Module.rank K V < ↑n
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_ciInf : ∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] {f : α → β},
  RightOrdContinuous f → ∀ {g : ι → α}, BddBelow (Set.range g) → f (⨅ i, g i) = ⨅ i, f (g i)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_injective : ∀ {V : Type u}, Function.Injective SimpleGraph.edgeSet
-- Mathlib.Data.PFun
PFun.preimage_inter : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : Set β), f.preimage (s ∩ t) ⊆ f.preimage s ∩ f.preimage t
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.contDiffWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiff 𝕜 n f → ContDiffWithinAt 𝕜 n f s x
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.basis.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} [inst_1 : NeZero n] {ι : Type u_4} (b : Module.Basis ι ℤ G),
  ModN.basis b =
    {
      repr :=
        LinearEquiv.ofBijective
          (AddMonoidHom.toZModLinearMap n
            (((LinearMap.lsmul ℤ G) ↑n).range.liftQ
                (Finsupp.mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap ∘ₗ ↑b.repr) ⋯).toAddMonoidHom)
          ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsSeparated
-- Mathlib.Logic.Equiv.Nat
Equiv.boolProdNatEquivNat_symm_apply : ∀ (n : ℕ), Equiv.boolProdNatEquivNat.symm n = (n.bodd, n.div2)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_dite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {P : Prop}
  [inst_2 : Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (if h : P then g h else g' h) =
    if h : P then CategoryTheory.MonoidalCategoryStruct.tensorHom f (g h)
    else CategoryTheory.MonoidalCategoryStruct.tensorHom f (g' h)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
monoidHomOfForallMemZpowers.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g)
  {g' : G'} (hg' : orderOf g' ∣ orderOf g),
  monoidHomOfForallMemZpowers hg hg' = { toFun := fun x => g' ^ Classical.choose ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Lean.Meta.Constructions.CasesOn
Lean.mkCasesOn : Lean.Name → Lean.MetaM Unit
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.norm_fourierSMulRight_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V), ‖VectorFourier.fourierSMulRight L f v‖ ≤ 2 * Real.pi * ‖L‖ * ‖v‖ * ‖f v‖
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- If a coalgebra morphism has an inverse, it is a coalgebra isomorphism.  -/
BialgEquiv.ofBialgHom : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] →
                    (f : A →ₐc[R] B) →
                      (g : B →ₐc[R] A) → f.comp g = BialgHom.id R B → g.comp f = BialgHom.id R A → A ≃ₐc[R] B
-- Init.Data.String.Substring
Substring.Raw.Internal.extractImpl : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Substring.Raw
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.mk : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) →
        (d : ℕ) →
          (hd : x.dim = d + 1) →
            (index : Fin (d + 1)) →
              SSet.prodStdSimplex.pairingCore.IsIndex x hd index.succ → SSet.prodStdSimplex.pairingCore.Type₁ k n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.instEssSurjCompPre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) [F.EssSurj], (CategoryTheory.CostructuredArrow.pre F G S).EssSurj
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- Given a functor `p : N ⥤ C`, this is the functor `C ⥤ Type w` which sends
`X : C` to the colimit of types of morphisms `p.obj U ⟶ X` for `U : N`.  -/
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          CategoryTheory.Functor N C → [CategoryTheory.InitiallySmall N] → CategoryTheory.Functor C (Type w)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.ne_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r : R}, v₁ r ≠ 0 ↔ v₂ r ≠ 0
-- Std.Http.Protocol.H1.Reader
/-- State waiting to be able to read new data.
 -/
Std.Http.Protocol.H1.Reader.State.pending : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.noConfusionType : Sort v✝ → Lean.Lsp.DiagnosticSeverity → Lean.Lsp.DiagnosticSeverity → Sort v✝