mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A topological space `X` is compactly generated if a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
uCompactlyGeneratedSpace_of_isOpen : ∀ {X : Type w} [tX : TopologicalSpace X],
  (∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) → IsOpen s) → UCompactlyGeneratedSpace X
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- The canonical projections maps  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.π : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [inst_4 : CategoryTheory.MonoidalClosed V] →
              {F G H : CategoryTheory.Functor C V} →
                CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H →
                  (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)
-- Init.GrindInstances.Ring.UInt
/-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`. -/
UInt16.ofNat_mod_size' : ∀ {x : ℕ}, UInt16.ofNat (x % 65536) = UInt16.ofNat x
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.mk : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M], ((nhds 0).HasBasis (fun N => ↑N ∈ nhds 0) fun N => ↑N) → IsLinearTopology R M
-- Init.Data.List.Perm
List.perm_cons_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l → l.Perm (a :: l.erase a)
-- Mathlib.Order.Filter.Cofinite
/-- The cofinite filter is the filter of subsets whose complements are finite.  -/
Filter.cofinite : {α : Type u_2} → Filter α
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion.lift_comp_incl : ∀ {V W : SemiNormedGrp} [inst : CompleteSpace W.carrier] [inst_1 : T0Space W.carrier] (f : V ⟶ W),
  CategoryTheory.CategoryStruct.comp SemiNormedGrp.completion.incl (SemiNormedGrp.completion.lift f) = f
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.comp : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f)
  (hh : Nat.RecursiveIn O h),
  Nat.RecursiveIn.below hf → motive f hf → Nat.RecursiveIn.below hh → motive h hh → Nat.RecursiveIn.below ⋯
-- Init.Data.SInt.Lemmas
Int8.pow_succ : ∀ (x : Int8) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
/-- **Alias** of `Matrix.GeneralLinearGroup.center_eq_range_scalar`.

---

The center of `GL n R` is the image of `Rˣ`.  -/
Matrix.GeneralLinearGroup.center_eq_range_units : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Subgroup.center (GL n R) = (Matrix.GeneralLinearGroup.scalar n).range
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.parts.injEq : ∀ (p p_1 : Array Lean.Lsp.InlayHintLabelPart),
  (Lean.Lsp.InlayHintLabel.parts p = Lean.Lsp.InlayHintLabel.parts p_1) = (p = p_1)
-- Mathlib.Order.Minimal
Minimal.not_prop_of_ssubset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Minimal P s → t ⊂ s → ¬P t
-- Init.Data.Option.Attach
Option.attach_eq_some : ∀ {α : Type u_1} (o : Option α) (x : { x // o = some x }), o.attach = some x
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.piecewise.congr_simp : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (x x_1 : Π₀ (i : ι), β i),
  x = x_1 →
    ∀ (y y_1 : Π₀ (i : ι), β i),
      y = y_1 →
        ∀ (s s_1 : Set ι),
          s = s_1 →
            ∀ {inst_1 : (i : ι) → Decidable (i ∈ s)} [inst_2 : (i : ι) → Decidable (i ∈ s_1)],
              x.piecewise y s = x_1.piecewise y_1 s_1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is an `AddSemigroup` under pointwise operations if `α` is.  -/
Set.addSemigroup : {α : Type u_2} → [AddSemigroup α] → AddSemigroup (Set α)
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_lt : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, ⌊a⌋ < z ↔ a < ↑z
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.sum.inj : ∀ {e : Q(ℕ)} {x x_1 : Mathlib.Tactic.Ring.Common.ExSumNat e},
  Mathlib.Tactic.Ring.Common.ExBaseNat.sum x = Mathlib.Tactic.Ring.Common.ExBaseNat.sum x_1 → x = x_1
-- Mathlib.Analysis.Normed.Operator.Prod
ContinuousOn.prod_mapL : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {M₄ : Type u_8}
  [inst_1 : SeminormedAddCommGroup M₁] [inst_2 : NormedSpace 𝕜 M₁] [inst_3 : SeminormedAddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜 M₂] [inst_5 : SeminormedAddCommGroup M₃] [inst_6 : NormedSpace 𝕜 M₃]
  [inst_7 : SeminormedAddCommGroup M₄] [inst_8 : NormedSpace 𝕜 M₄] {X : Type u_9} [inst_9 : TopologicalSpace X]
  {f : X → M₁ →L[𝕜] M₂} {g : X → M₃ →L[𝕜] M₄} {s : Set X},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => (f x).prodMap (g x)) s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C) {Z : D} (h : F.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj A) (F.obj B)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd A B)) h
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.subset_addSpan : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α}, s ⊆ s.addSpan
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append_head : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j k l : ι} {w₁ : Monoid.CoprodI.NeWord M i j}
  {hne : j ≠ k} {w₂ : Monoid.CoprodI.NeWord M k l}, (w₁.append hne w₂).head = w₁.head
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_subset_closure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, intrinsicClosure 𝕜 s ⊆ closure s
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
/-- Box-additive map sending each box `I` to the continuous linear endomorphism
`x ↦ (volume I).toReal • x`.  -/
BoxIntegral.BoxAdditiveMap.volume : {ι : Type u_1} →
  [Fintype ι] →
    {E : Type u_2} →
      [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] E) ⊤
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instNeg : {α : Type u_1} → [Neg α] → Neg (Colex α)
-- Mathlib.LinearAlgebra.FreeModule.ModN
/-- The quotient map `G → G / nG`.  -/
ModN.mkQ : {G : Type u_1} → [inst : AddCommGroup G] → (n : ℕ) → G →+ ModN G n
-- Mathlib.Probability.StrongLaw
MeasureTheory.AEStronglyMeasurable.truncation : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ}, MeasureTheory.AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.mk : ∀ {M : Type u} [inst : HAdd M M M] [inst_1 : LE M] [inst_2 : Std.IsPreorder M],
  (∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c) → Lean.Grind.OrderedAdd M
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addGroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : Neg M₁]
  [inst_4 : Sub M₁] [inst_5 : SMul ℤ M₁] [inst_6 : AddGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Injective.addGroup f hf one mul inv div npow zpow =
    { toSubNegMonoid := Function.Injective.subNegMonoid f hf one mul inv div npow zpow, neg_add_cancel := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The lattice invariant `g₂ := 60 G₄`.  -/
PeriodPair.g₂ : PeriodPair → ℂ
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vsub_vsub_le : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (p₁ p₂ p₃ p₄ : P), nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
-- Mathlib.Order.Lattice
SemilatticeSup.toMax : {α : Type u} → [SemilatticeSup α] → Max α
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_ofFin : ∀ (n : Fin USize.size) (h : System.Platform.numBits = 64), (USize.ofFin n).toBitVec64 h = { toFin := h ▸ n }
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_eq_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {hst : s = t}
  (x : ↥(SubAddAction.ofFixingAddSubgroup M s)), ↑((SubAddAction.ofFixingAddSubgroup_of_eq M hst) x) = ↑x
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [inst_1 : ∀ (i : I), NormOneClass (B i)]
  [Nonempty I], NormOneClass ↥(lp B ⊤)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
  CategoryTheory.CategoryStruct.comp ((G.obj (Opposite.op Y₁)).whiskerLeft (F.map f)) (adj₂.adj Y₁).counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (G.map f.op) (F.obj X₁))
      (adj₂.adj X₁).counit
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalarsEquiv_symm_apply : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (p : Submodule R M)
  (a : ↥p), (Submodule.restrictScalarsEquiv S R M p).symm a = a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The type of sections of a sheaf of modules.  -/
SheafOfModules.sections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → SheafOfModules R → Type (max u₁ v)
-- Init.Data.Array.Range
Array.range'_inj : ∀ {s n s' n' : ℕ}, Array.range' s n = Array.range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_normalizer_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ Subgroup.normalizer ↑K ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_3} {J : Type u_4} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} B] [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤))
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderLimitsOfShape J]
  [CategoryTheory.Limits.HasLimit (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))],
  CategoryTheory.Limits.HasLimit D
-- Lean.Level
/-- Converts a natural number to the corresponding `Lean.Level`.

This is intentionally in the `Lean` namespace to avoid polluting the `Nat` namespace. Note that
after `open Lean`, `n.toLevel` will work for `n : Nat`.
 -/
Lean.Nat.toLevel : ℕ → Lean.Level
-- Mathlib.Algebra.Order.Group.Finset
Finset.nsmul_inf' : ∀ {ι : Type u_1} {M : Type u_3} [inst : LinearOrder M] [inst_1 : AddMonoid M] [AddLeftMono M] [AddRightMono M]
  (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty), n • s.inf' hs f = s.inf' hs fun a => n • f a
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.toList_empty : ∀ {β : Type u_1}, (Std.Iter.empty β).toList = []
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff_null'`. -/
MeasureTheory.measureReal_diff_null' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ.real (s₁ ∩ s₂) = 0 →
    autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_sdiff_null'._auto_1 → μ.real (s₁ \ s₂) = μ.real s₁
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.toArray_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.toList.toArray = t.toArray
-- Mathlib.Data.DFinsupp.Order
DFinsupp.disjoint_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → LinearOrder (α i)]
  [inst_2 : ∀ (i : ι), IsBotZeroClass (α i)] [inst_3 : DecidableEq ι] {f g : Π₀ (i : ι), α i},
  Disjoint f g ↔ Disjoint f.support g.support
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.single_kroneckerTMul_single : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] [inst_5 : DecidableEq l] [inst_6 : DecidableEq m] [inst_7 : DecidableEq n]
  [inst_8 : DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β),
  Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.single i₁ j₁ a) (Matrix.single i₂ j₂ b) =
    Matrix.single (i₁, i₂) (j₁, j₂) (a ⊗ₜ[R] b)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.mem_basicOpen_den : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↑(ProjectiveSpectrum.top 𝒜))
  (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl),
  x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den
-- Mathlib.Order.Partition.Basic
Partition.Rel.right_mem : ∀ {α : Type u_1} {x y : α} {u : Set α} {P : Partition u}, P.Rel x y → y ∈ u
-- Lean.Parser.Types
Lean.Parser.instBEqError : BEq Lean.Parser.Error
-- Aesop.Tree.State
Aesop.RappRef.markSubtreeIrrelevant : Aesop.RappRef → BaseIO Unit
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Any `K`-Lipschitz map from a subset `s` of a metric space `α` to a finite-dimensional real
vector space `E'` can be extended to a Lipschitz map on the whole space `α`, with a slightly worse
constant `lipschitzExtensionConstant E' * K`.  -/
LipschitzOnWith.extend_finite_dimension : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedSpace ℝ E'] [inst_3 : FiniteDimensional ℝ E'] {s : Set α} {f : α → E'} {K : NNReal},
  LipschitzOnWith K f s → ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ Set.EqOn f g s
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullbackWithin_eq_of_not_isInvertible : ∀ {𝕜 : 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] {s : Set E}
  {f : E → F} {x : E}, ¬(fderivWithin 𝕜 f s x).IsInvertible → ∀ (V : F → F), VectorField.pullbackWithin 𝕜 f V s x = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- See also `rpow_neg` for a version with `(x ^ y)⁻¹` in the RHS.  -/
Real.rpow_neg_eq_inv_rpow : ∀ (x y : ℝ), x ^ (-y) = x⁻¹ ^ y
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.IsAlt.eq_iff : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁}, B₁.IsAlt → ∀ {x y : M₁}, (B₁ x) y = 0 ↔ (B₁ y) x = 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
a prime if `p ^ (k  + 1) ≠ 2`.  -/
IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  p ^ (k + 1) ≠ 2 → Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given a presheaf of modules `M`, this is a constructor for the type `M.Elements`.  -/
PresheafOfModules.elementsMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → (M : PresheafOfModules R) → (X : Cᵒᵖ) → ↑(M.obj X) → M.Elements
-- Init.Data.Array.MapIdx
List.mapIdx_toArray : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l : List α}, Array.mapIdx f l.toArray = (List.mapIdx f l).toArray
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_of_retractArrow : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c}
  {f : K ⟶ L} {f' : K' ⟶ L'} (h : CategoryTheory.RetractArrow f f') [inst_2 : ∀ (i : ι), K.HasHomology i]
  [inst_3 : ∀ (i : ι), L.HasHomology i] [inst_4 : ∀ (i : ι), K'.HasHomology i] [inst_5 : ∀ (i : ι), L'.HasHomology i]
  [QuasiIso f'], QuasiIso f
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftHomotopy_apply : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E))
  (H_0 : ∀ (a : A), H (0, a) = p (f a)) (ta : ↑unitInterval × A),
  (cov.liftHomotopy H f H_0) ta =
    (cov.liftPath (H.comp ((ContinuousMap.id ↑unitInterval).prodMk (ContinuousMap.const (↑unitInterval) ta.2))) (f ta.2)
        ⋯)
      ta.1
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- Maps elements of `α` to their immediate successor.
 -/
Std.PRange.UpwardEnumerable.succ : {α : Type u} → [inst : Std.PRange.UpwardEnumerable α] → [Std.PRange.InfinitelyUpwardEnumerable α] → α → α
-- Mathlib.ModelTheory.Substructures
/-- The underlying set of this substructure  -/
FirstOrder.Language.Substructure.carrier : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → L.Substructure M → Set M
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_eq_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P},
  midpoint R x y = z ↔ (AffineEquiv.pointReflection R z) x = y
-- Mathlib.Algebra.Algebra.Operations
Submodule.coe_set_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I : Submodule R A} {N : Submodule R M}, ↑I • N = I • N
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An open immersion of PresheafedSpaces is an open embedding `f : X ⟶ U ⊆ Y` of the underlying
spaces, such that the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : AlgebraicGeometry.PresheafedSpace C} → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A family of maps from `left a` to `right (J.fst a)`  -/
CategoryTheory.Limits.MultispanIndex.fst : {J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.Limits.MultispanIndex J C) → (a : J.L) → self.left a ⟶ self.right (J.fst a)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Except.toBool.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (a : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (a : ε) → motive (Except.error a)),
  (match Except.error a with
    | Except.ok a => h_1 a
    | Except.error a => h_2 a) =
    h_2 a
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.instHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGrp
-- Std.Http.Protocol.H1
/-- Consumes one header line in `needHeader` state.

On a regular field line it delegates to `processParsedHeader`; on an empty line
it finalizes header processing via `processHeaders`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processNeedHeader : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → ℕ → Std.Http.Protocol.H1.Machine dir
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instMinOfOrd : {α : Type u} → [Ord α] → Min α
-- Mathlib.RingTheory.Unramified.Finite
/-- A finite-type `R`-algebra `S` is (formally) unramified iff there exists a `t : S ⊗[R] S` satisfying
1. `t` annihilates every `1 ⊗ s - s ⊗ 1`.
2. the image of `t` is `1` under the map `S ⊗[R] S → S`.

See `Algebra.FormallyUnramified.iff_exists_tensorProduct`.
This is the choice of such a `t`.
 -/
Algebra.FormallyUnramified.elem : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → [Algebra.FormallyUnramified R S] → [Algebra.EssFiniteType R S] → TensorProduct R S S
-- Mathlib.Algebra.Regular.Defs
IsAddRightRegular.eq_1 : ∀ {R : Type u_1} [inst : Add R] (c : R), IsAddRightRegular c = Function.Injective fun x => x + c
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_singleton_comm : ∀ {α : Type u_1} {a b : α}, a ≠ b → ∀ (s : Set α), insert a (s \ {b}) = insert a s \ {b}
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.inv_mem_of_isUnit : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : DivisionMonoid α] [inst_2 : SubmonoidClass C α] {S : C}
  {a : ↥S}, IsUnit a → (↑a)⁻¹ ∈ S
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.atEnd : ∀ {p : ℕ} {s : Substring.Raw}, s.Valid → (s.atEnd { byteIdx := p } = true ↔ p = s.toString.utf8ByteSize)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) {X Y : Cᵒᵖ}
  (f : X ⟶ Y),
  (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).map f =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f.unop)
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.checkNoRevert : Lean.Meta.Grind.Params → Lean.CoreM Unit
-- Mathlib.Data.Set.Basic
Set.union_assoc : ∀ {α : Type u} (a b c : Set α), a ∪ b ∪ c = a ∪ (b ∪ c)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsPath ↔ p.support.Nodup
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decomp : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] [inst_6 : TopologicalSpace W]
  [inst_7 : IsTopologicalAddGroup V] [inst_8 : IsTopologicalAddGroup W] (f : V →ᴬ[R] W),
  ⇑f = ⇑f.contLinear + Function.const V (f 0)