mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.homIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C},
  (h.homIso W).hom = TypeCat.ofHom fun f => (t.extend f.down).ι
-- Mathlib.NumberTheory.NumberField.House
NumberField.house.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K),
  NumberField.house α = ‖(NumberField.canonicalEmbedding K) α‖
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset.eq_1 : ∀ {σ : Type u_1} (R : Type u_4) [inst : CommSemiring R] (s : Finset (σ →₀ ℕ)),
  MvPowerSeries.truncFinset R s =
    { toFun := fun p => ∑ x ∈ s, (MvPolynomial.monomial x) ((MvPowerSeries.coeff x) p), map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_X_le : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.degree ≤ 1
-- Init.Data.UInt.BasicAux
/-- Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.toUInt32 : UInt64 → UInt32
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instInhabited : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → Inhabited (LieDerivation R L M)
-- Lean.Expr
/-- Instantiates loose bound variable `0` in `e` using the expression `subst`,
where in particular a loose `Expr.bvar i` at binding depth `d` is instantiated with `subst` if `i = d`,
and otherwise it is replaced with `Expr.bvar (i - 1)`; non-loose bound variables are not touched.

If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order,
then conceptually `instantiate1` is instantiating the last one of these and reindexing the remaining ones.

This function is equivalent to `instantiate e #[subst]`, but it avoids allocating an array.

See the documentation for `Lean.Expr.instantiate` for a description of instantiation.
In short, during instantiation the loose bound variables in `subst` have their own de Bruijn indices updated to account
for the binding depth of the replaced loose bound variable.
 -/
Lean.Expr.instantiate1 : Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.mk : Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.DoIfView
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.congr_of_eventuallyEq_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → ContMDiffWithinAt I I' n f₁ s x
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_univ : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.exradius Finset.univ = s.inradius
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanFileProgressParams.toJson : Lean.Lsp.LeanFileProgressParams → Lean.Json
-- Init.Data.Nat.Basic
Nat.add_one_add_one_ne_one : ∀ {a : ℕ}, a + 1 + 1 ≠ 1
-- Mathlib.Data.List.Infix
List.IsSuffix.nodup : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₂.Nodup → l₁.Nodup
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.dual_id : ∀ {α : Type u_2} [inst : CompleteLattice α],
  CompleteLatticeHom.dual (CompleteLatticeHom.id α) = CompleteLatticeHom.id αᵒᵈ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Get the `n`th vertex from a walk, where `n` is generally expected to be
between `0` and `p.length`, inclusive.
If `n` is greater than or equal to `p.length`, the result is the path's endpoint.  -/
SimpleGraph.Walk.getVert : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → ℕ → V
-- Mathlib.Algebra.Order.Group.Basic
zsmul_left_strictAnti : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α},
  a < 0 → StrictAnti fun n => n • a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_add_right : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {b : α}, (fun x => x + b) '' t = (fun x => x + -b) ⁻¹' t
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Composition of affine maps acts as applying the two functions.  -/
AffineMap.comp_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1), (f.comp g) p = f (g p)
-- Mathlib.CategoryTheory.Functor.Basic
/-- `Functor C D` represents a functor between categories `C` and `D`.

To apply a functor `F` to an object use `F.obj X`, and to a morphism use `F.map f`.

The axiom `map_id` expresses preservation of identities, and
`map_comp` expresses functoriality.  -/
CategoryTheory.Functor : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] → (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max v₁ v₂ u₁ u₂)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitInv_app_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C), e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.compRight : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                {E' : Type u_4} →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} E'] →
                    (F : CategoryTheory.Functor C E) →
                      (F' : CategoryTheory.Functor D E) →
                        [CategoryTheory.Localization.Lifting L W F F'] →
                          (G : CategoryTheory.Functor E E') →
                            CategoryTheory.Localization.Lifting L W (F.comp G) (F'.comp G)
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.instFloorDiv : {ι : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : AddCommMonoid α] →
        [inst_1 : PartialOrder α] →
          [inst_2 : AddCommMonoid β] →
            [inst_3 : PartialOrder β] → [inst_4 : SMulZeroClass α β] → [FloorDiv α β] → FloorDiv α (ι →₀ β)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factor.eq_1 : ∀ {R : Type u} [inst : Ring R] {S T : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] (H : S ≤ T),
  Ideal.Quotient.factor H = Ideal.Quotient.lift S (Ideal.Quotient.mk T) ⋯
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.intervalIntegral_re : ∀ {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → ∫ (x : ℝ) in a..b, RCLike.re (f x) ∂μ = RCLike.re (∫ (x : ℝ) in a..b, f x ∂μ)
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindFunctor'_obj : ∀ (k : Type u) {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (A : Rep.{max u w, u, v} k G), (Rep.coindFunctor' k φ).obj A = Rep.coind' φ A
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The coweight space representation of automorphisms  -/
RootPairing.Equiv.coweightHom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → P.Aut →* (N ≃ₗ[R] N)ᵐᵒᵖ
-- Init.Data.Array.Basic
Array.eraseIdx.induct : ∀ {α : Type u} (motive : (xs : Array α) → (i : ℕ) → i < xs.size → Prop),
  (∀ (xs : Array α) (i : ℕ) (h : i < xs.size) (h_1 : i + 1 < xs.size),
      let xs' := xs.swap (i + 1) i h_1 h;
      motive xs' (i + 1) ⋯ → motive xs i h) →
    (∀ (xs : Array α) (i : ℕ) (h : i < xs.size), ¬i + 1 < xs.size → motive xs i h) →
      ∀ (xs : Array α) (i : ℕ) (h : i < xs.size), motive xs i h
-- Mathlib.Analysis.Normed.Module.Ray
norm_injOn_ray_right : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {y : F},
  y ≠ 0 → Set.InjOn norm {x | SameRay ℝ x y}
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.denote.match_1.splitter : (motive : Lean.Grind.CommRing.Mon → Sort u_1) →
  (x : Lean.Grind.CommRing.Mon) →
    (Unit → motive Lean.Grind.CommRing.Mon.unit) →
      ((p : Lean.Grind.CommRing.Power) → (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m)) →
        motive x
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_mul_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x y : K)
  (hx : 0 ≤ ArchimedeanClass.mk x) (hy : 0 ≤ ArchimedeanClass.mk y),
  ArchimedeanClass.FiniteElement.mk x hx * ArchimedeanClass.FiniteElement.mk y hy =
    ArchimedeanClass.FiniteElement.mk (x * y) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every regular monomorphism is a monomorphism.  -/
CategoryTheory.RegularMono.mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (h : CategoryTheory.RegularMono f),
  CategoryTheory.Mono f
-- Mathlib.Logic.Basic
forall₃_imp : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop},
  (∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c) →
    (∀ (a : α) (b : β a) (c : γ a b), p a b c) → ∀ (a : α) (b : β a) (c : γ a b), q a b c
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.getKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getKey! ⟨{ size := size, buckets := buckets }, hm⟩ a =
    Std.DHashMap.Internal.AssocList.getKey! a buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Algebra.Notation.Pi.Basic
/-- A congruence lemma for `Pi.single`, specialized for the non-dependent case. Without this,
`simp` can't rewrite in the first and third argument (`i` and `j`) because of dependence.
See also https://github.com/leanprover/lean4/issues/12478.
 -/
Pi.single_congr : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : Zero M] {i₁ i₂ : ι},
  i₁ = i₂ → ∀ {x₁ x₂ : M}, x₁ = x₂ → ∀ {j₁ j₂ : ι}, j₁ = j₂ → Pi.single i₁ x₁ j₁ = Pi.single i₂ x₂ j₂
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴}
  {toNatTrans : CategoryTheory.NatTrans F.toFunctor G.toFunctor}
  {isHomLift' :
    autoParam (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans.app a))
      CategoryTheory.BasedNatTrans.isHomLift'._autoParam}
  {toNatTrans_1 : CategoryTheory.NatTrans F.toFunctor G.toFunctor}
  {isHomLift'_1 :
    autoParam (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans_1.app a))
      CategoryTheory.BasedNatTrans.isHomLift'._autoParam},
  { toNatTrans := toNatTrans, isHomLift' := isHomLift' } = { toNatTrans := toNatTrans_1, isHomLift' := isHomLift'_1 } →
    toNatTrans = toNatTrans_1
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_tensorAssoc_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
  (Q₃ : QuadraticForm R M₃) (x : TensorProduct R (TensorProduct R M₁ M₂) M₃),
  (Q₁.tmul (Q₂.tmul Q₃)) ((TensorProduct.assoc R M₁ M₂ M₃) x) = ((Q₁.tmul Q₂).tmul Q₃) x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- The notation for StronglyMeasurable giving the measurable space instance explicitly.  -/
MeasureTheory.«termStronglyMeasurable[_]» : Lean.ParserDescr
-- Mathlib.Order.SupClosed
infClosure_empty : ∀ {α : Type u_3} [inst : SemilatticeInf α], infClosure ∅ = ∅
-- Mathlib.LinearAlgebra.Contraction
dualTensorHomEquivOfBasis_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b : Module.Basis ι R M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (x : TensorProduct R (Module.Dual R M) N),
  (dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x
-- Init.Data.List.Basic
List.concat.eq_1 : ∀ {α : Type u} (x : α), [].concat x = [x]
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instCopyDiscardCategory : CategoryTheory.CopyDiscardCategory SFinKer
-- Mathlib.Analysis.Complex.Liouville
/-- **Cauchy's estimate for derivatives**:  If `f` is complex differentiable on an open disc of
radius `R > 0`, is continuous on its closure, and its values on the boundary circle of this disc
are bounded from above by `C`, then the norm of its `n`-th derivative at the center is at most
`n.factorial * C / R ^ n`.  -/
Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F}
  (n : ℕ),
  0 < R →
    DiffContOnCl ℂ f (Metric.ball c R) →
      (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖iteratedDeriv n f c‖ ≤ ↑n.factorial * C / R ^ n
-- Lean.Environment
Lean.Kernel.Exception.declTypeMismatch.injEq : ∀ (env : Lean.Kernel.Environment) (decl : Lean.Declaration) (givenType : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (decl_1 : Lean.Declaration) (givenType_1 : Lean.Expr),
  (Lean.Kernel.Exception.declTypeMismatch env decl givenType =
      Lean.Kernel.Exception.declTypeMismatch env_1 decl_1 givenType_1) =
    (env = env_1 ∧ decl = decl_1 ∧ givenType = givenType_1)
-- Init.Data.Option.Lemmas
Option.any_map : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool},
  Option.any p (Option.map f x) = Option.any (fun a => p (f a)) x
-- Lean.Attributes
Lean.instInhabitedAttributeImplCore : Inhabited Lean.AttributeImplCore
-- Init.Data.SInt.Lemmas
ISize.toInt_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toInt = b.toInt
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.toList_eq.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → ((stop : ℕ) → motive (some stop)) → (Unit → motive none) → motive x
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.startsWith.match_1.eq_1 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x y : Lean.Grind.AC.Var)
  (h_1 : (x y : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y))
  (h_2 :
    (x y : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x_1 : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_1))
  (h_4 :
    (x : Lean.Grind.AC.Var) →
      (s₂ : Lean.Grind.AC.Seq) →
        (y : Lean.Grind.AC.Var) →
          (s₁ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁)),
  (match Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => h_1 x y
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s => h_2 x y s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_1 => h_3 x s x_1
    | Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ => h_4 x s₂ y s₁) =
    h_1 x y
-- Init.Data.BitVec.Lemmas
/-- if the msb is false, the arithmetic shift right equals logical shift right  -/
BitVec.sshiftRight_eq_of_msb_false : ∀ {w : ℕ} {x : BitVec w} {s : ℕ}, x.msb = false → x.sshiftRight s = x >>> s
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.mk.injEq : ∀ {G : Type u_1} [inst : AddCommGroup G] (toAddSubmonoid : AddSubmonoid G)
  (eq_zero_of_mem_of_neg_mem' : ∀ {a : G}, a ∈ toAddSubmonoid.carrier → -a ∈ toAddSubmonoid.carrier → a = 0)
  (toAddSubmonoid_1 : AddSubmonoid G)
  (eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : G}, a ∈ toAddSubmonoid_1.carrier → -a ∈ toAddSubmonoid_1.carrier → a = 0),
  ({ toAddSubmonoid := toAddSubmonoid, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'_1 }) =
    (toAddSubmonoid = toAddSubmonoid_1)
-- Mathlib.Topology.CompactOpen
Homeomorph.continuousMapOfUnique_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique X] (y : Y)
  (x : X), (Homeomorph.continuousMapOfUnique y) x = y
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt32HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Tactic.Algebraize
Mathlib.Tactic.Algebraize.Config.mk.inj : ∀ {properties properties_1 : Bool},
  { properties := properties } = { properties := properties_1 } → properties = properties_1
-- Mathlib.Probability.IdentDistrib
/-- Two functions defined on two (possibly different) measure spaces are identically distributed if
their image measures coincide. This only makes sense when the functions are ae measurable
(as otherwise the image measures are not defined), so we require this as well in the definition.  -/
ProbabilityTheory.IdentDistrib : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] →
          [MeasurableSpace γ] →
            (α → γ) →
              (β → γ) →
                autoParam (MeasureTheory.Measure α) ProbabilityTheory.IdentDistrib._auto_1 →
                  autoParam (MeasureTheory.Measure β) ProbabilityTheory.IdentDistrib._auto_3 → Prop
-- Mathlib.Data.FunLike.IsApply
IsSMulApply.mk : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : FunLike F α β]
  [inst_1 : SMul M β] [inst_2 : SMul M F], (∀ (f : F) (r : M) (x : α), (r • f) x = r • f x) → IsSMulApply M F α β
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_nil_iff : ∀ {m n : ℕ}, (m<...n).toArray = #[] ↔ n ≤ m + 1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateRow_sum_aux : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  {j : n} (s : Finset n), j ∉ s → ∀ (c : n → R) (a : R), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.lt → motive Ordering.lt) →
      (x = Ordering.eq → motive Ordering.eq) → (x = Ordering.gt → motive Ordering.gt) → motive x
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.q.eq_1 : ∀ (p : ℕ), LucasLehmer.q p = ⟨(mersenne p).minFac, ⋯⟩
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_getModify_bind : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (s : σ) (f : σ → σ) (mx : σ → m α),
  (do
      set s
      let x ← getModify f
      mx x) =
    do
    set (f s)
    mx s
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpConst : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff.sizeOf_spec : ∀ (k : ℕ) (c : Lean.Meta.Grind.Arith.Linear.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff k c) = 1 + sizeOf k + sizeOf c
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.instInhabited : (V : Type u_1) → [inst : CategoryTheory.ReflQuiver V] → Inhabited (V ⥤rq V)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.integer.coe_span_singleton_eq_setOfPred_le_v_coe : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  (x : ↥v.integer), ↑(Ideal.span {x}) = {y | v ↑y ≤ v ↑x}
-- Mathlib.Data.Fin.Basic
/-- If working with more than two elements, we can always pick a third distinct from two existing
elements.  -/
Fin.exists_ne_and_ne_of_two_lt : ∀ {n : ℕ} (i j : Fin n), 2 < n → ∃ k, k ≠ i ∧ k ≠ j
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.cons.inj : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {tree : Std.DTreeMap.Internal.Impl α β}
  {next : Std.DTreeMap.Internal.Zipper α β} {k_1 : α} {v_1 : β k_1} {tree_1 : Std.DTreeMap.Internal.Impl α β}
  {next_1 : Std.DTreeMap.Internal.Zipper α β},
  Std.DTreeMap.Internal.Zipper.cons k v tree next = Std.DTreeMap.Internal.Zipper.cons k_1 v_1 tree_1 next_1 →
    k = k_1 ∧ v ≍ v_1 ∧ tree = tree_1 ∧ next = next_1
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.instCompleteLinearOrderLexForall : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedLT ι] → CompleteLinearOrder (Lex ((i : ι) → (fun i => α i) i))
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] [F.Faithful],
  ((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).Faithful
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.equivOfIso_apply : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) (a : ↑V), (CategoryTheory.Quiv.equivOfIso e) a = e.hom.obj a
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.sup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : SemilatticeSup β] → [ContinuousSup β] → Max C(α, β)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism theorem** for commutative rings, surjective case.  -/
RingHom.quotientKerEquivOfSurjective : {R : Type u} →
  {S : Type v} →
    [inst : Ring R] → [inst_1 : Semiring S] → {f : R →+* S} → Function.Surjective ⇑f → R ⧸ RingHom.ker f ≃+* S
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A point in a collinear set of points lies in the affine span of any two distinct points of
that set.  -/
Collinear.mem_affineSpan_of_mem_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P},
  Collinear k s → ∀ {p₁ p₂ p₃ : P}, p₁ ∈ s → p₂ ∈ s → p₃ ∈ s → p₁ ≠ p₂ → p₃ ∈ line[k, p₁, p₂]