mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso.match_1.eq_2 : ∀ {ι : Type u_1} [inst : LinearOrder ι]
  (motive : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι) → Sort u_2)
  (a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R)
  (h_1 :
    (a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left a))
  (h_2 :
    (a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R) →
      motive (CategoryTheory.Limits.WalkingMultispan.right a)),
  (match CategoryTheory.Limits.WalkingMultispan.right a with
    | CategoryTheory.Limits.WalkingMultispan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMultispan.right a => h_2 a) =
    h_2 a
-- Mathlib.Order.Monotone.Basic
monotoneOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_ofNat_mul_add' : ∀ {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],
  toIocMod hp (OfNat.ofNat m * p + a) b = OfNat.ofNat m * p + toIocMod hp a b
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.copy_eq : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (f' : A → B) (h : f' = ⇑f),
  f.copy f' h = f
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- Given a morphism `f : M →ₗ[R] A`, `IsSymmetricAlgebra f` is a proposition saying that the
algebra homomorphism from `SymmetricAlgebra R M` to `A` is bijective.  -/
IsSymmetricAlgebra : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {A : Type u_3} → [inst_3 : CommSemiring A] → [inst_4 : Algebra R A] → (M →ₗ[R] A) → Prop
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.i_f_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) {Z : C}
  (h : (CochainComplex.cm5b.I K).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.cm5b.i f).f n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f n)
        (CategoryTheory.CategoryStruct.comp
          ((CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))).v n n ⋯) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.ι (K.X n)) h
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.k_mul_j : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.k * q.j = c₃ • q.i
-- Batteries.Data.FloatArray
/-- Inner loop for `mapMUnsafe`.  -/
FloatArray.mapMUnsafe.loop : {m : Type → Type u_1} → [Monad m] → (Float → m Float) → FloatArray → USize → USize → m FloatArray
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.sup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMinOn f s a → IsLocalMinOn g s a → IsLocalMinOn (fun x => f x ⊔ g x) s a
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.Config.mk : Lean.Meta.Rewrite.Config → Bool → Bool → Bool → Mathlib.Tactic.GRewrite.Config
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {km : α},
  t.max? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.mk.sizeOf_spec : ∀ {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 y : CategoryTheory.Limits.CategoricalPullback F G} [inst_3 : SizeOf A] [inst_4 : SizeOf B] [inst_5 : SizeOf C]
  (fst : x.fst ⟶ y.fst) (snd : x.snd ⟶ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map fst) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd))
      CategoryTheory.Limits.CategoricalPullback.Hom.w._autoParam),
  sizeOf { fst := fst, snd := snd, w := w } = 1 + sizeOf fst + sizeOf snd + sizeOf w
-- Mathlib.Logic.Equiv.Set
Equiv.ofPreimageEquiv_symm_apply : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
  (a : β), (Equiv.ofPreimageEquiv e).symm a = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a)).snd
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.prodComonad.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X X_1 : C),
  X = X_1 →
    ∀ [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
      CategoryTheory.prodComonad X = CategoryTheory.prodComonad X_1
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The program that evaluates code `c` with continuation `k`. This expects an initial state where
`trList v` is on `main`, `trContStack k` is on `stack`, and `aux` and `rev` are empty.
See the section documentation for details.  -/
Turing.PartrecToTM2.trNormal : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Λ'
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher : {ρ : Type} → ρ → String.Slice → Type
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTop_id : ∀ {α : Type u_1} [inst : Lattice α], (LatticeHom.id α).withTop = LatticeHom.id (WithTop α)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.unique_quotient_iff_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M},
  Nonempty (Unique (M ⧸ p)) ↔ p = ⊤
-- Mathlib.Data.Part
Part.eq_iff_of_dom : ∀ {α : Type u_1} {a b : Part α} (ha : a.Dom) (hb : b.Dom), a.get ha = b.get hb ↔ a = b
-- Mathlib.LinearAlgebra.Projection
/-- Projection to a submodule along a complement. It is the unique
linear map `f : E → p` such that `f x = x` for `x ∈ p` and `f x = 0` for `x ∈ q`.

For the projection from `E` to `E`, see `Submodule.projection`. See also:
* `Submodule.projectionOntoL` and `Submodule.projectionL` for the continuous versions.
* `Submodule.orthogonalProjection` and `Submodule.orthogonalProjectionOnto` for the projections
  along the orthogonal subspace.

See also `LinearMap.linearProjOfIsCompl`.  -/
Submodule.projectionOnto : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → E →ₗ[R] ↥p
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_strongLT`. -/
StrongLT.le : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i}, StrongLT a b → a ≤ b
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂_unique : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R]
  [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    MvPowerSeries.HasEval a →
      ∀ {ε : MvPowerSeries σ R → S},
        Continuous ε → (∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p) → ε = MvPowerSeries.eval₂ φ a
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.IsMultiplicative], W.ContainsIdentities
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instHashableBVUnOp : Hashable Std.Tactic.BVDecide.BVUnOp
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_eq_empty`. -/
Set.diff_eq_empty : ∀ {α : Type u_1} {s t : Set α}, s \ t = ∅ ↔ s ⊆ t
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_injective : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R], Function.Injective ⇑(algebraMap R (QuadraticAlgebra R a b))
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_lt_coeff_mul : ∀ {R : Type u} {m n : ℕ} [inst : Semiring R] {p q : Polynomial R},
  p.natDegree + q.natDegree < m + n → (p * q).coeff (m + n) = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.curryAddEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N] (m : M)
  (n : N) (r : R),
  AddMonoidAlgebra.curryAddEquiv.symm (AddMonoidAlgebra.single m (AddMonoidAlgebra.single n r)) =
    AddMonoidAlgebra.single (m, n) r
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.openDecls : Lean.Elab.Term.SavedContext → List Lean.OpenDecl
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2⁻¹
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_dvd_subst_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → Bool
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, k ∈ m.insert k v
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.subsingleton_liftStruct_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) [CategoryTheory.Epi i], Subsingleton sq.LiftStruct
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
GrpCat.binaryProductLimitCone_cone_pt : ∀ (G H : GrpCat), (G.binaryProductLimitCone H).cone.pt = GrpCat.of (↑G × ↑H)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_prod : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (f₁ : A →A[R] B)
  (f₂ : A →A[R] C), ↑(f₁.prod f₂) = (↑f₁).prod ↑f₂
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformContinuous_coe : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous SetLike.coe
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.prevn.eq_2 : ∀ (x : Substring.Raw) (x_1 : String.Pos.Raw) (i : ℕ), x.prevn i.succ x_1 = x.prevn i (x.prev x_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).isEmpty = false
-- Lean.Message
Lean.MessageDataContext : Type
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedGeneralTheorem.default : Mathlib.Meta.FunProp.GeneralTheorem
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instMulAdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Mul (AdicCompletion.AdicCauchySequence I R)
-- Mathlib.Dynamics.Flow
Flow.forwardOrbit_eq_range_nonneg : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) [inst_3 : Preorder τ] [inst_4 : AddLeftMono τ] (x : α),
  ϕ.forwardOrbit x = Set.range fun t => ϕ.toFun (↑t) x
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal_app_0 : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (H :
    ∀ (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ }))
      (y : Y.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) x) =
          (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) y →
        f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) y →
          f₁
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op)) y)
  (hσ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) (f₀ x))
  (hY : Y.StrictSegal),
  (SSet.Truncated.liftOfStrictSegal f₀ f₁ hδ₁ hδ₀ H hσ hY).app
      (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) =
    TypeCat.ofHom f₀
-- Init.GetElem
/-- The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
panics if `i` is out of bounds.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]!` in identifiers is `getElem!`. -/
«term__[_]_!» : Lean.TrailingParserDescr
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.le : Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrictHom_apply : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Type u_5} [inst_1 : SetLike S M] [inst_2 : SubmonoidClass S M] (M' : S)
  (A : Type u_6) [inst_3 : CommMonoid A] (f : M →* A), (MonoidHom.domRestrictHom M' A) f = f.domRestrict M'
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_last : ∀ {n : ℕ} {α : Type u_3} (f : Fin (n + 1) → α), (Fin.last n).removeNth f = Fin.init f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = false → Std.DTreeMap.Raw.Const.get? t a = none
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) {Z : AlgebraicGeometry.Scheme}
  (h : ↑↑V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataT U V)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯))
        (CategoryTheory.CategoryStruct.comp (I.glueDataObjι V) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))
      (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.one_lt_opow : ∀ {a b : Ordinal.{u_1}}, 1 < a ^ b ↔ 1 < a ∧ b ≠ 0
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- In case of an even dimension, the sign of the determinant of `g : PGL(n, R)` is well-defined.  -/
Matrix.ProjGenLinGroup.signDet : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] →
          [Fact (Even (Fintype.card n))] →
            [inst_4 : LinearOrder R] → [IsStrictOrderedRing R] → Matrix.ProjGenLinGroup n R →* SignTypeˣ
-- Init.Data.BitVec.Lemmas
BitVec.cpop_cast : ∀ {w v : ℕ} (x : BitVec w) (h : w = v), (BitVec.cast h x).cpop = BitVec.cast h x.cpop
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.not_adj_sum_inl_inr : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (v : V) (w : W),
  ¬(G ⊕g H).Adj (Sum.inl v) (Sum.inr w)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.ofEq_homInvId : ∀ {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} {hom' : SSet.Edge y₀ y₁}
  (I : hom.InvStruct) (hhom : hom.edge = hom'.edge), (I.ofEq hhom).homInvId = I.homInvId.ofEq hhom ⋯ ⋯
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_uIcc_left : ∀ {α : Type u_1} [inst : Lattice α] {a b x : α}, x ∈ Set.uIcc a b → Set.uIcc a x ⊆ Set.uIcc a b
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) (i : 𝒰.I₀),
  d.transitionMap (CategoryTheory.CategoryStruct.id i) =
    (CategoryTheory.MorphismProperty.Over.mapId ⊤ (𝒰.X i)
            (AlgebraicGeometry.Scheme.Cover.trans 𝒰 (CategoryTheory.CategoryStruct.id i)) ⋯).hom.app
      (d.cocone i).pt
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.failed.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {err err_1 : Std.Http.Protocol.H1.Error},
  Std.Http.Protocol.H1.Event.failed err = Std.Http.Protocol.H1.Event.failed err_1 → err = err_1
-- Lean.Expr
Lean.instInhabitedExprStructEq.default : Lean.ExprStructEq
-- Mathlib.NumberTheory.Padics.WithVal
/-- The `p`-adic numbers are isomorphic as uniform spaces to the completion of the rationals at
the `p`-adic valuation.  -/
Padic.withValUniformEquiv : {p : ℕ} → [inst : Fact (Nat.Prime p)] → (Rat.padicValuation p).Completion ≃ᵤ ℚ_[p]
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.Hom.hom_nsmul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.AddMon C}
  [inst_3 : CategoryTheory.IsCommAddMonObj N.X] (f : M ⟶ N) (n : ℕ), (n • f).hom = n • f.hom
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.id_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C) (i j : M.ι),
  CategoryTheory.CategoryStruct.id M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.or_left_comm : ∀ (x y z : ℕ), x ||| (y ||| z) = y ||| (x ||| z)
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- A monoidal equivalence between skeletal monoidal categories induces a monoid isomorphism.  -/
CategoryTheory.Skeletal.mulEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (e : C ≌ D) →
              [e.functor.Monoidal] →
                (hC : CategoryTheory.Skeletal C) →
                  (hD : CategoryTheory.Skeletal D) →
                    have x := CategoryTheory.monoidOfSkeletalMonoidal hC;
                    have x_1 := CategoryTheory.monoidOfSkeletalMonoidal hD;
                    C ≃* D
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
/-- Let `f : E → F` be a function differentiable in a neighborhood of `a`.
If $Df(x) = O(‖x - a‖ ^ r)$ as `x → a`, where `r ≥ 0`,
then $f(x) - f(a) = O(‖x - a‖ ^ {r + 1})$ as `x → a`.  -/
sub_isBigO_norm_rpow_add_one_of_fderiv : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ},
  0 ≤ r →
    (∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) →
      (fderiv ℝ f =O[nhds a] fun x => ‖x - a‖ ^ r) → (fun x => f x - f a) =O[nhds a] fun x => ‖x - a‖ ^ (r + 1)
-- Std.Async.Basic
/-- Returns the `BaseAsync` computation inside a `Task α`, so it can be awaited.
 -/
Std.Async.BaseAsync.async : {α : Type} → Std.Async.BaseAsync α → optParam Task.Priority Task.Priority.default → Std.Async.BaseAsync (Task α)
-- Mathlib.Computability.Primrec.Basic
Primrec.of_equiv_symm : ∀ {α : Type u_1} [inst : Primcodable α] {β : Type u_4} {e : β ≃ α}, Primrec ⇑e.symm
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant], μ.neg = μ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.ofList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.Raw.ofList [] cmp = ∅
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.aeval_eq : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} (p : Polynomial R),
  (Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) p
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a product is 1 and the function is 1 except possibly at one
point, it is 1 everywhere on the `Finset`.  -/
Finset.eq_one_of_prod_eq_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M} {a : ι},
  ∏ x ∈ s, f x = 1 → (∀ x ∈ s, x ≠ a → f x = 1) → ∀ x ∈ s, f x = 1
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.Iso.mk_hom : ∀ {α β : FinBddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat),
  (FinBddDistLat.Iso.mk e).hom =
    FinBddDistLat.ofHom
      (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ},
  CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X =
    CategoryTheory.FunctorToTypes.shrink.{w, v, v, u} (CategoryTheory.coyoneda.obj X)
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Runs a `DSimpM` computation with the given methods, configuration, and state.
The `cache` and `numSteps` from `s` are preserved (cache entries persist across
invocations because results are not context-dependent).  -/
Lean.Meta.Sym.DSimp.DSimpM.run : {α : Type} →
  Lean.Meta.Sym.DSimp.DSimpM α →
    optParam Lean.Meta.Sym.DSimp.Methods { } →
      optParam Lean.Meta.Sym.DSimp.Config { } →
        optParam Lean.Meta.Sym.DSimp.State { } → Lean.Meta.Sym.SymM (α × Lean.Meta.Sym.DSimp.State)
-- Init.Prelude
/-- `` `hygieneInfo `` is the node kind of the `Lean.Parser.hygieneInfo` parser, which produces an
“invisible token” that captures the hygiene information at the current point without parsing
anything.

They can be used to generate identifiers (with `Lean.HygieneInfo.mkIdent`) as if they were
introduced in a macro's input, rather than by its implementation.
 -/
Lean.hygieneInfoKind : Lean.SyntaxNodeKind