mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Tactic.Unreachable
/-- This tactic causes a panic when run (at compile time).
(This is distinct from `exact unreachable!`, which inserts code which will panic at run time.)

It is intended for tests to assert that a tactic will never be executed, which is otherwise an
unusual thing to do (and the `unreachableTactic` linter will give a warning if you do).

The `unreachableTactic` linter has a special exception for uses of `unreachable!`.
```
example : True := by trivial <;> unreachable!
```
 -/
Batteries.Tactic.unreachable : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the kernel condition for `i`  -/
CategoryTheory.ShortComplex.LeftHomologyData.wi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData), CategoryTheory.CategoryStruct.comp self.i S.g = 0
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lflip_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  {R₀ : Type u_14} [inst_12 : Semiring R₀] [inst_13 : Module R₀ P] [inst_14 : SMulCommClass S₂ R₀ P]
  [inst_15 : SMulCommClass R₂ R₀ P] (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P), LinearMap.lflip f = f.flip
-- Init.Data.Int.DivMod.Lemmas
Int.add_fdiv_of_dvd_right : ∀ {a b c : ℤ}, c ∣ b → (a + b).fdiv c = a.fdiv c + b.fdiv c
-- Init.Prelude
instMonadWithReaderOfMonadWithReaderOf : (ρ : Type u) → (m : Type u → Type v) → [MonadWithReaderOf ρ m] → MonadWithReader ρ m
-- Lean.Data.Lsp.Internal
/-- Full import closure of the file.  -/
Lean.Lsp.LeanImportClosureParams.importClosure : Lean.Lsp.LeanImportClosureParams → Array Lean.Lsp.DocumentUri
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.rightUnitor_inv_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv) m = m ⊗ₜ[R] 1
-- Init.Data.String.Defs
/-- Appends all the strings in a list of strings, in order.

Use `String.intercalate` to place a separator string between the strings in a list.

Examples:
* `String.join ["gr", "ee", "n"] = "green"`
* `String.join ["b", "", "l", "", "ue"] = "blue"`
* `String.join [] = ""`
 -/
String.join : List String → String
-- Mathlib.LinearAlgebra.Dimension.RankNullity
Submodule.disjoint_ker_of_finrank_le : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_2} R] [StrongRankCondition R] [IsDomain R] [Module.IsTorsionFree R M] {N : Type u_1}
  [inst_7 : AddCommGroup N] [inst_8 : Module R N] {L : Submodule R M} [Module.Finite R ↥L] (f : M →ₗ[R] N),
  Module.finrank R ↥L ≤ Module.finrank R ↥(Submodule.map f L) → Disjoint L f.ker
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower such that `E / F` is purely inseparable,
if `S` is an intermediate field of `K / F` which is separable over `F`, then `S` and `E` are
linearly disjoint over `F`.  -/
IntermediateField.linearDisjoint_of_isPurelyInseparable_of_isSeparable : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K] [IsPurelyInseparable F E]
  (S : IntermediateField F K) [Algebra.IsSeparable F ↥S], S.LinearDisjoint E
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.restrictScalars.eq_1 : ∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : Ring S] [inst_3 : Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M]
  [inst_7 : Module R M] [inst_8 : IsScalarTower R S M] [inst_9 : Module.IsTorsionFree R S] (b : Module.Basis ι S M),
  Module.Basis.restrictScalars R b = Module.Basis.span ⋯
-- Std.Data.ExtDTreeMap.Lemmas
/-- Variant of `get!_map` that holds without `LawfulEqCmp`.  -/
Std.ExtDTreeMap.Const.get!_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → γ} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.map f t) k =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.ExtDTreeMap.Const.get? t k) ⋯).get!
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.leftSMul.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.ModObj.leftSMul M X =
    CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.ModObj.smul
      (CategoryTheory.SemiCartesianMonoidalCategory.snd M X)
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.finrank_quotient_sup_span_singleton : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {W : Submodule K V} {v : V},
  v ∉ W → Module.finrank K (V ⧸ W ⊔ K ∙ v) + 1 = Module.finrank K (V ⧸ W)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.succ_mem_succ_iff : ∀ {α : Type u} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {hi a : α}, (Std.PRange.succ a ∈ *...Std.PRange.succ hi) ↔ a ∈ *...hi
-- Mathlib.Algebra.GroupWithZero.Basic
/-- Multiplying `a` by its inverse and then by itself results in `a`
(whether or not `a` is zero).  -/
mul_inv_mul_cancel : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a * a⁻¹ * a = a
-- Mathlib.Data.List.Permutation
Nat.factorial.eq_def : ∀ (x : ℕ),
  x.factorial =
    match x with
    | 0 => 1
    | n.succ => n.succ * n.factorial
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt64
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ} (h : t.WF),
  Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.filterMap f t) k fallback =
    ((Std.DTreeMap.Raw.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Algebra.GroupWithZero.Basic
zpow_add' : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀} {m n : ℤ},
  a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0 → a ^ (m + n) = a ^ m * a ^ n
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IicExtend_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) (x : ↑(Set.Iic b)),
  Set.IicExtend f ↑x = f x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, a ∈ m.erase k → a ∈ m
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The additive subgroup of elements `x : G` such that `f x = g x`  -/
AddMonoidHom.eqLocus : {G : Type u_1} → [inst : AddGroup G] → {M : Type u_7} → [inst_1 : AddMonoid M] → (G →+ M) → (G →+ M) → AddSubgroup G
-- Mathlib.Data.Matrix.Mul
Matrix.pow_col_eq_zero_of_le : ∀ {n : Type u_3} {R : Type u_7} [inst : Semiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M : Matrix n n R}
  {k l : ℕ} {i : n}, (M ^ k).col i = 0 → k ≤ l → (M ^ l).col i = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp] {k : α},
  Std.ExtDTreeMap.Const.insertManyIfNewUnit t [k] = t.insertIfNew k ()
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιNormalizedChainComplex_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })),
  CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) ((X.normalizedChainComplex R).d (n + 1) n) =
    ∑ i,
      (-1) ^ ↑i •
        X.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOverHom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (f : X ⟶ Y) [inst_3 : CategoryTheory.HomIsOver f S],
  (CategoryTheory.OverClass.asOverHom S f).left = f
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.congr_right : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
  {g₁ g₂ : α → F}, f =O[l] g₁ → (∀ (x : α), g₁ x = g₂ x) → f =O[l] g₂
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.save : Lean.Expr → Lean.Expr → Lean.Meta.Sym.M✝ Lean.Expr
-- Init.Data.SInt.Lemmas
Int8.toInt64_toISize : ∀ (n : Int8), n.toISize.toInt64 = n.toInt64
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.CostructuredArrow.isSeparating_inverseImage_proj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (S : CategoryTheory.Functor C D) (T : D) {P : CategoryTheory.ObjectProperty C},
  P.IsSeparating → (P.inverseImage (CategoryTheory.CostructuredArrow.proj S T)).IsSeparating
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet_limit : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {a : Ordinal.{u}},
  Order.IsSuccLimit a → CantorBendixson.iteratedDerivedSet s a = ⋂ b, CantorBendixson.iteratedDerivedSet s ↑b
-- Mathlib.RingTheory.FreeCommRing
/-- Lift a map `α → R` to an additive group homomorphism `FreeCommRing α → R`.  -/
FreeCommRing.lift : {α : Type u} → {R : Type v} → [inst : CommRing R] → (α → R) ≃ (FreeCommRing α →+* R)
-- Mathlib.Order.Sublattice
Sublattice.subtype_comp_inclusion : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α} (h : L ≤ M),
  M.subtype.comp (Sublattice.inclusion h) = L.subtype
-- Mathlib.Order.Bounds.Basic
isGLB_iff_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s
-- Mathlib.NumberTheory.LocalField.Basic
/-- Given a topological field `K` equipped with an equivalence class of valuations (a `ValuativeRel`),
we say that it is a non-archimedean local field if the topology comes from the given valuation,
and it is locally compact and non-discrete.

This implies the following typeclasses via `inferInstance`
- `IsValuativeTopology K`
- `LocallyCompactSpace K`
- `IsTopologicalDivisionRing K`
- `ValuativeRel.IsNontrivial K`
- `ValuativeRel.IsRankLeOne K`
- `ValuativeRel.IsDiscrete K`
- `IsDiscreteValuationRing 𝒪[K]`
- `Finite 𝓀[K]`

Assuming we have a compatible `UniformSpace K` instance
(e.g. via `IsTopologicalAddGroup.toUniformSpace` and `isUniformAddGroup_of_addCommGroup`) then
- `CompleteSpace K`
- `CompleteSpace 𝒪[K]`
 -/
IsNonarchimedeanLocalField : (K : Type u_1) → [inst : Field K] → [ValuativeRel K] → [TopologicalSpace K] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Preconnected.ofBoxProdLeft : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [Nonempty β],
  (G □ H).Preconnected → G.Preconnected
-- Mathlib.Algebra.Ring.Defs
NonAssocSemiring.toMulZeroOneClass : {α : Type u} → [self : NonAssocSemiring α] → MulZeroOneClass α
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_subtype_span_singleton : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M}
  (x : ↥p), Submodule.map p.subtype (R ∙ x) = R ∙ ↑x
-- Init.Data.Array.Subarray
/-- The starting index of the region of interest (inclusive).  -/
Std.Slice.Internal.SubarrayData.start : {α : Type u} → Std.Slice.Internal.SubarrayData α → ℕ
-- Mathlib.Algebra.Star.Rat
Rat.instStarRing : StarRing ℚ
-- Mathlib.Topology.UniformSpace.Compact
Filter.HasBasis.lebesgue_number_lemma_nhds : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)}
  {U : α → Set α},
  (uniformity α).HasBasis p V →
    IsCompact K → (∀ x ∈ K, U x ∈ nhds x) → ∃ i, p i ∧ ∀ x ∈ K, ∃ y, UniformSpace.ball x (V i) ⊆ U y
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.divisionMonoid : {α : Type u} → [SubtractionMonoid α] → DivisionMonoid (Multiplicative α)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.user.sizeOf_spec : sizeOf Lean.Meta.Grind.EMatchTheoremKind.user = 1
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.interSmaller.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.interSmaller l₁ l₂ =
    List.foldl (fun sofar kv => Std.Internal.List.interSmallerFn l₁ sofar kv.fst) [] l₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_of_le : ∀ (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ),
  autoParam (d ≤ n) SSet.hasDimensionLT_of_le._auto_1 → X.HasDimensionLT n
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
  CategoryTheory.IsIso (D.diagramOverOpenπ U i)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
AdjoinRoot.Minpoly.toAdjoin.eq_1 : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  AdjoinRoot.Minpoly.toAdjoin R x = AdjoinRoot.liftAlgHom (minpoly R x) (Algebra.ofId R ↥R[x]) ⟨x, ⋯⟩ ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of a primitive root is
`1` if `n ≠ 2`.  -/
IsPrimitiveRoot.norm_eq_one : ∀ {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [inst : CommRing L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ n →
    ∀ [IsDomain L] [IsCyclotomicExtension {n} K L],
      n ≠ 2 → Irreducible (Polynomial.cyclotomic n K) → (Algebra.norm K) ζ = 1
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- If a set is von Neumann bounded with respect to a smaller field,
then it is also von Neumann bounded with respect to a larger field.
See also `Bornology.IsVonNBounded.restrict_scalars` below.  -/
Bornology.IsVonNBounded.extend_scalars : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_6} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (𝕝 : Type u_7) [inst_3 : NontriviallyNormedField 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] [inst_5 : Module 𝕝 E]
  [inst_6 : TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {s : Set E},
  Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕝 s
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_pi_iff_lt_zero : ∀ {z : ℂ}, z.arg = Real.pi ↔ z < 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If there are zero morphisms, any terminal object is a zero object.  -/
CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasTerminal C], CategoryTheory.Limits.HasZeroObject C
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.tryTheorem? : Lean.Expr → Lean.Meta.SimpTheorem → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Batteries.Data.Fin.Lemmas
Fin.eq_false_of_isNone_findRev? : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, (Fin.findRev? p).isNone = true → p i = false
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities.mk : Option Bool → Option Lean.Lsp.ResolveSupport → Lean.Lsp.InlayHintClientCapabilities
-- Lean.Parser.Command
Lean.Parser.Command.optionValue.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {c : ℕ}, Std.DHashMap.Raw.Const.toList (Std.DHashMap.Raw.emptyWithCapacity c) = []
-- Mathlib.Analysis.Normed.Group.Basic
enorm_zero : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E], ‖0‖ₑ = 0
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.zero_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (i : ℕ), ↑0 i = 0
-- Mathlib.InformationTheory.Hamming
Hamming.instAddCommGroup : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → AddCommGroup (β i)] → AddCommGroup (Hamming β)
-- Mathlib.Algebra.Order.Interval.Basic
instSubNonemptyInterval : {α : Type u_2} →
  [inst : Preorder α] →
    [inst_1 : AddCommSemigroup α] → [inst_2 : Sub α] → [OrderedSub α] → [AddLeftMono α] → Sub (NonemptyInterval α)
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableOn_fun_neg_iff : ∀ {𝕜 : 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] {f : E → F}
  {s : Set E}, DifferentiableOn 𝕜 (fun y => -f y) s ↔ DifferentiableOn 𝕜 f s
-- Mathlib.Order.Bounds.Image
/-- The image under an antitone function of a set which is bounded below is bounded
above.  -/
Antitone.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {s : Set α}, BddBelow s → BddAbove (f '' s)
-- Lean.Util.FindExpr
/-- Returns true if `e` occurs in `t`  -/
Lean.Expr.occurs : Lean.Expr → Lean.Expr → Bool
-- Mathlib.Order.BooleanAlgebra.Basic
codisjoint_iff_compl_le_left : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Codisjoint x y ↔ yᶜ ≤ x
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_ofClass : ∀ {S : Type u_3} {G : Type u_4} [inst : AddGroup G] [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G] (s : S),
  ↑(AddSubgroup.ofClass s) = ↑s
-- Lean.Attributes
Lean.TagAttribute.ext : Lean.TagAttribute → Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoMod hp (a - OfNat.ofNat m * p) b = toIcoMod hp a b - OfNat.ofNat m * p
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMapOnAlgHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (X : Set R)
  (p : Polynomial R), (Polynomial.toContinuousMapOnAlgHom X) p = p.toContinuousMapOn X
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.liftOn₂_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (Localization.r S) (a, b) (a', b') → (Localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d')
  (a c : M) (b d : ↥S), ((Localization.monoidOf S).mk' a b).liftOn₂ ((Localization.monoidOf S).mk' c d) f H = f a b c d
-- Mathlib.LinearAlgebra.Reflection
Module.preReflection.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M)
  (f : Module.Dual R M), Module.preReflection x f = LinearMap.id - LinearMap.smulRight f x
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_filterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {f : β → n (ULift.{w, 0} Bool)} [inst_1 : Monad n] [inst_2 : MonadAttach n] [LawfulMonad n] [MonadLiftT m n],
  (Std.Iter.filterM f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let __do_lift ← MonadAttach.attach (f out)
      match __do_lift with
        | ⟨{ down := false }, hf⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterM f it') ⋯))
        | ⟨{ down := true }, hf⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.filterM f it') out ⋯))
    | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterM f it') ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Group.Pi.Basic
Pi.leftCancelSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → LeftCancelSemigroup (f i)] → LeftCancelSemigroup ((i : I) → f i)
-- Init.Data.Order.Lemmas
Std.instSymmEqBoolBeqTrueOfLawfulOrderBEq : ∀ {α : Type u} [inst : BEq α] [inst_1 : LE α] [Std.LawfulOrderBEq α], Std.Symm fun x1 x2 => (x1 == x2) = true
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.differentiable_cos : Differentiable ℂ Complex.cos
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.eq_of_mem_uIcc_of_mem_uIcc : ∀ {α : Type u_1} [inst : DistribLattice α] {a b c : α}, a ∈ Set.uIcc b c → b ∈ Set.uIcc a c → a = b
-- Mathlib.Data.Int.Sqrt
/-- `sqrt z` is the square root of an integer `z`. If `z` is positive, it returns the largest
integer `r` such that `r * r ≤ n`. If it is negative, it returns `0`. For example, `sqrt (-1) = 0`,
`sqrt 1 = 1`, `sqrt 2 = 1`  -/
Int.sqrt : ℤ → ℤ
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_top : ∀ {G : Type u_2} [inst : AddGroup G], ⊤.op = ⊤
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The functoriality of the diagrams attached to `data : F.PreOneHypercoverDenseData X`
with respect to morphisms in `C₀ᵒᵖ ⥤ A`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {A : Type u'} →
            [inst_2 : CategoryTheory.Category.{v', u'} A] →
              {X : C} →
                (data : F.PreOneHypercoverDenseData X) →
                  {P Q : CategoryTheory.Functor C₀ᵒᵖ A} →
                    (P ⟶ Q) → ((data.multicospanIndex P).multicospan ⟶ (data.multicospanIndex Q).multicospan)
-- Mathlib.Tactic.Linter.Style
/-- Configuration option for the "longLine" linter. This option determines the
maximum allowed length of a line before the linter emits a warning.
This defaults to 100.  -/
Mathlib.Linter.linter.style.longLine.maxLineLength : Lean.Option ℕ
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ'_map : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.Luroth.Φ'✝ E) =
    RatFunc.Luroth.b✝ E • Polynomial.map (algebraMap (↥E) (RatFunc K)) (RatFunc.Luroth.φ✝ E)
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- Construct limit data for a binary product in `GrpCat`, using `GrpCat.of (G × H)`  -/
GrpCat.binaryProductLimitCone : (G H : GrpCat) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The forgetful functor from additive commutative groups to additive groups is fully faithful.  -/
AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).FullyFaithful
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instInhabited : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → Inhabited (ClopenUpperSet α)