mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.cfcAux_id : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian), hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A
-- Mathlib.Order.OrderDual
OrderDual.instMinOfMax : (α : Type u_2) → [h : Max α] → Min αᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (β_ Y Y').hom =
    CategoryTheory.CategoryStruct.comp (β_ X X').hom (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.arrowCongrEquiv.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ σ₁₃_1 : R₁ →+* R₃} (e_σ₁₃ : σ₁₃ = σ₁₃_1) [inst_5 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  {M₁ : Type u_4} [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5}
  [inst_8 : TopologicalSpace M₂] [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃]
  [inst_11 : AddCommMonoid M₃] {M₄ : Type u_7} [inst_12 : TopologicalSpace M₄] [inst_13 : AddCommMonoid M₄]
  [inst_14 : Module R₁ M₁] [inst_15 : Module R₂ M₂] [inst_16 : Module R₃ M₃] {R₄ : Type u_8} [inst_17 : Semiring R₄]
  [inst_18 : Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [inst_19 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_20 : RingHomInvPair σ₄₃ σ₃₄] {σ₂₄ σ₂₄_1 : R₂ →+* R₄} (e_σ₂₄ : σ₂₄ = σ₂₄_1) {σ₁₄ : R₁ →+* R₄}
  [inst_21 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_22 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_23 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (e₁₂ e₁₂_1 : M₁ ≃SL[σ₁₂] M₂),
  e₁₂ = e₁₂_1 → ∀ (e₄₃ e₄₃_1 : M₄ ≃SL[σ₄₃] M₃), e₄₃ = e₄₃_1 → e₁₂.arrowCongrEquiv e₄₃ = e₁₂_1.arrowCongrEquiv e₄₃_1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_singleton_iff : ∀ {k m n : ℤ}, (m<...n).toList = [k] ↔ n = m + 2 ∧ m + 1 = k
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrixAux_eq`. -/
BilinearForm.toMatrixAux_eq : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁), (LinearMap.BilinForm.toMatrixAux ⇑b) B = (LinearMap.BilinForm.toMatrix b) B
-- Aesop.EMap
Aesop.instInhabitedEMap : {a : Type u_1} → Inhabited (Aesop.EMap a)
-- Mathlib.Algebra.Group.Center
Set.addCenter.eq_1 : ∀ (M : Type u_1) [inst : Add M], Set.addCenter M = {z | IsAddCentral z}
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instVAdd : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → VAdd α (LowerSet α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false → t.isEmpty = false
-- Mathlib.Data.Nat.ChineseRemainder
_private.Mathlib.Data.Nat.ChineseRemainder.0.Nat.chineseRemainderOfList.match_1.eq_1 : ∀ {ι : Type u_1} (s : ι → ℕ) (motive : (x : List ι) → List.Pairwise (Function.onFun Nat.Coprime s) x → Sort u_2)
  (x : List.Pairwise (Function.onFun Nat.Coprime s) [])
  (h_1 : (x : List.Pairwise (Function.onFun Nat.Coprime s) []) → motive [] x)
  (h_2 : (i : ι) → (l : List ι) → (co : List.Pairwise (Function.onFun Nat.Coprime s) (i :: l)) → motive (i :: l) co),
  (match [], x with
    | [], x => h_1 x
    | i :: l, co => h_2 i l co) =
    h_1 x
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The type of objects of the category `Fib S` for each `S`.  -/
HasFibers.Fib : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳} →
        (p : CategoryTheory.Functor 𝒳 𝒮) → [self : HasFibers p] → 𝒮 → Type u₃
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contractElem_eq_self : ∀ {α : Type u_1} {M : Matroid α} {e : α}, e ∉ M.E → M.contract {e} = M
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.instLawfulMonad : LawfulMonad FreeAbelianGroup
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks₁₁_diagonal : ∀ {l : Type u_1} {m : Type u_2} {α : Type u_12} [inst : DecidableEq l] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  (v : l ⊕ m → α), (Matrix.diagonal v).toBlocks₁₁ = Matrix.diagonal fun i => v (Sum.inl i)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- If `α` has a unique term, then the product of magmas `α → M` is isomorphic to `M`.  -/
MulEquiv.funUnique : (α : Type u_2) → (M : Type u_4) → [inst : Mul M] → [Unique α] → (α → M) ≃* M
-- Init.Data.Rat.Lemmas
Rat.ceil_sub_one : ∀ {x : ℚ}, (x - 1).ceil = x.ceil - 1
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Algebra.TensorProduct.tensorTensorTensorComm.congr_simp : ∀ (R : Type uR) (R' : Type u_1) (S : Type uS) (T : Type u_2) (A : Type uA) (B : Type uB) (C : Type uC) (D : Type uD)
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : CommSemiring T] [inst_16 : Algebra R T]
  [inst_17 : Algebra T A] [inst_18 : IsScalarTower R T A] [inst_19 : SMulCommClass S T A] [inst_20 : Algebra S T]
  [inst_21 : IsScalarTower S T A] [inst_22 : CommSemiring R'] [inst_23 : Algebra R R'] [inst_24 : Algebra R' T]
  [inst_25 : Algebra R' A] [inst_26 : Algebra R' B] [inst_27 : IsScalarTower R R' A] [inst_28 : SMulCommClass S R' A]
  [inst_29 : SMulCommClass R' S A] [inst_30 : IsScalarTower R' T A] [inst_31 : IsScalarTower R R' B],
  Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D =
    Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey? k = none
-- Mathlib.Logic.Equiv.Sum
/-- Inhabited types are equivalent to `Option β` for some `β` by identifying `default` with `none`.
 -/
Equiv.sigmaEquivOptionOfInhabited : (α : Type u) → [Inhabited α] → [DecidableEq α] → (β : Type u) × (α ≃ Option β)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_pow : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x : R) (n : ℕ), WithAbs.toAbs v (x ^ n) = WithAbs.toAbs v x ^ n
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.fderiv_of_isOpen : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {m n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → IsOpen s → m + 1 ≤ n → ContDiffOn 𝕜 m (fderiv 𝕜 f) s
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight_inv : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.mulETransformRight e⁻¹ x = (Finset.mulETransformLeft e x.swap).swap
-- Mathlib.Computability.MyhillNerode
Language.leftQuotient_accepts : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.accepts.leftQuotient = M.acceptsFrom ∘ M.eval
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.foldrAux.eq_def : ∀ {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : String.Pos.Raw),
  String.Legacy.foldrAux f a s i begPos =
    if h : begPos < i then
      have this := ⋯;
      have i := String.Pos.Raw.prev s i;
      have a := f (String.Pos.Raw.get s i) a;
      String.Legacy.foldrAux f a s i begPos
    else a
-- Lean.Elab.DefView
Lean.Elab.DefView.type? : Lean.Elab.DefView → Option Lean.Syntax
-- Lean.ProjFns
Lean.instInhabitedProjectionFunctionInfo : Inhabited Lean.ProjectionFunctionInfo
-- Mathlib.Topology.MetricSpace.HolderNorm
memHolder_zero : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal}
  [inst_2 : Zero Y], MemHolder r 0
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.of_succ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 (n + 1) f s → ContDiffOn 𝕜 n f s
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfinitePos.not_infinitesimal : ∀ {x : ℝ*}, x.InfinitePos → ¬x.Infinitesimal
-- Mathlib.Order.Filter.Defs
Filter.mem_of_superset : ∀ {α : Type u_1} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
-- Mathlib.Algebra.Category.ModuleCat.Stalk
PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier : {X : TopCat} →
  {R : TopCat.Presheaf CommRingCat X} →
    (M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) →
      (x : ↑X) → Module ↑(R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.isLocalHom_singleOneAlgHom : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M], IsLocalHom MonoidAlgebra.singleOneAlgHom
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `f : X → Y` is Hölder continuous on `s` with a positive exponent `r`, then
`μH[d] (f '' s) ≤ C ^ d * μH[r * d] s`.  -/
HolderOnWith.hausdorffMeasure_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {C r : NNReal} {f : X → Y} {s : Set X},
  HolderOnWith C r f s →
    0 < r →
      ∀ {d : ℝ},
        0 ≤ d →
          (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤
            ↑C ^ d * (MeasureTheory.Measure.hausdorffMeasure (↑r * d)) s
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- The complex closed unit disc, denoted as `𝕔𝔻` within the Complex namespace  -/
Complex.UnitClosedDisc : Type
-- Init.Data.Ord.Basic
Ordering.swap_swap : ∀ {o : Ordering}, o.swap.swap = o
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instOne : {G : Type u_1} → [inst : Add G] → {a : G} → One (AddConstEquiv G G a a)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmop_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ), (β_ X Y).unmop = β_ Y.unmop X.unmop
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- **Alias** of the forward direction of `Asymptotics.isBigO_iff_exists_eq_mul`. -/
Asymptotics.IsBigO.exists_eq_mul : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
  u =O[l] v → ∃ φ, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
-- Mathlib.Data.Int.Order.Units
Int.isUnit_iff_abs_eq : ∀ {x : ℤ}, IsUnit x ↔ |x| = 1
-- Mathlib.Analysis.Normed.Group.Basic
norm_add_sub_norm_sub_le_two_mul : ∀ {E : Type u_8} [inst : SeminormedAddGroup E] (u v : E), ‖u + v‖ - ‖u - v‖ ≤ 2 * ‖v‖
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- If the condition `G.Adj v w` fails, then `card_commonNeighbors_le_degree` is
the best we can do in general.  -/
SimpleGraph.Adj.card_commonNeighbors_lt_degree : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {v w : V},
  G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) < G.degree v
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.ofBases : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {ι : Type u_3} (b : E → ι → Set E) (p : E → ι → Prop),
  (∀ (x : E), (nhds x).HasBasis (p x) (b x)) → (∀ (x : E) (i : ι), p x i → Convex 𝕜 (b x i)) → LocallyConvexSpace 𝕜 E
-- Init.Data.List.Nat.TakeDrop
List.take_add : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, List.take (i + j) l = List.take i l ++ List.take j (List.drop i l)
-- Init.Data.Int.Lemmas
Int.neg_ofNat_zero : -↑0 = 0
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.below.of_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsPrenex → Prop} {n : ℕ}
  {φ : L.BoundedFormula α n} (h : φ.IsQF), FirstOrder.Language.BoundedFormula.IsPrenex.below ⋯
-- Mathlib.Order.OrderDual
OrderDual.instPreorder : (α : Type u_2) → [Preorder α] → Preorder αᵒᵈ
-- Lean.Meta.ArgsPacker
/-- Given expression `e` of type `(x : A) → (y : B[x]) → … → (z : D[x,y]) → R[x,y,z]`
returns an expression of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2]`.
 -/
Lean.Meta.ArgsPacker.Unary.uncurry : Array Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.SuccPred.Basic
Order.Ioi_pred_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Set.Ioi (Order.pred a) = Set.Ici a
-- Mathlib.Order.Antichain
IsAntichain.image_iso : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → ∀ (φ : α ≃o β), IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lift.congr_simp : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (f f_1 : A →ₐ[S] C) (e_f : f = f_1)
  (g g_1 : B →ₐ[R] C) (e_g : g = g_1) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)),
  Algebra.TensorProduct.lift f g hfg = Algebra.TensorProduct.lift f_1 g_1 ⋯
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.has_univ : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α), d.Has Set.univ
-- Init.SimpLemmas
decide_not : ∀ {p : Prop} [g : Decidable p] [h : Decidable ¬p], (decide ¬p) = !decide p
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_conjTranspose : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} [inst : DecidableEq o] {α : Type u_14} [inst_1 : AddMonoid α]
  [inst_2 : StarAddMonoid α] (M : (i : o) → Matrix (m' i) (n' i) α),
  (Matrix.blockDiagonal' M).conjTranspose = Matrix.blockDiagonal' fun k => (M k).conjTranspose
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.filterMapM.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The morphism from the cone point of any other cone to the limit object.  -/
CategoryTheory.Limits.limit.lift : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            (c : CategoryTheory.Limits.Cone F) → c.pt ⟶ CategoryTheory.Limits.limit F
-- Mathlib.LinearAlgebra.Ray
smul_rayOfNeZero : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {G : Type u_5} [inst_5 : Group G] [inst_6 : DistribMulAction G M]
  [inst_7 : SMulCommClass R G M] (g : G) (v : M) (hv : v ≠ 0), g • rayOfNeZero R v hv = rayOfNeZero R (g • v) ⋯
-- Lean.Meta.Basic
/-- The binder annotation for the parameter.  -/
Lean.Meta.ParamInfo.binderInfo : Lean.Meta.ParamInfo → Lean.BinderInfo
-- Std.Time.DateTime
Std.Time.DateTime.instHSubDuration_1 : HSub Std.Time.DateTime Std.Time.Duration Std.Time.DateTime
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply_univ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α), (μ.restrict s) Set.univ = μ s
-- Lean.SubExpr
_private.Lean.SubExpr.0.Lean.SubExpr.Pos.ofStringCoord : String → Except String ℕ
-- Mathlib.Topology.Bornology.Basic
Bornology.IsCobounded.inter : ∀ {α : Type u_2} {x : Bornology α} {s t : Set α},
  Bornology.IsCobounded s → Bornology.IsCobounded t → Bornology.IsCobounded (s ∩ t)
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.conjExponent_eq : ∀ {p q : ℝ}, p.HolderConjugate q → p.conjExponent = q
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.adapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [mΒ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)]
  [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.Adapted f u
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₂_le_cocycles₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  groupCohomology.coboundaries₂ A ≤ groupCohomology.cocycles₂ A
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.alt.inj : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} {m : ι → M} {i j : ι} {hm : m i = m j} {hij : i ≠ j} {m_1 : ι → M}
  {i_1 j_1 : ι} {hm_1 : m_1 i_1 = m_1 j_1} {hij_1 : i_1 ≠ j_1},
  exteriorPower.presentation.Rels.alt m i j hm hij = exteriorPower.presentation.Rels.alt m_1 i_1 j_1 hm_1 hij_1 →
    m = m_1 ∧ i = i_1 ∧ j = j_1
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.instIsLowerSetWithLowerSet : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsLowerSet (Topology.WithLowerSet α)
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The horizontal composition of 2-squares.  -/
CategoryTheory.TwoSquare.hComp : {C₁ : Type u₁} →
  {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₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        {C₅ : Type u₅} →
                          {C₆ : Type u₆} →
                            [inst_4 : CategoryTheory.Category.{v₅, u₅} C₅] →
                              [inst_5 : CategoryTheory.Category.{v₆, u₆} C₆] →
                                {T' : CategoryTheory.Functor C₂ C₅} →
                                  {R' : CategoryTheory.Functor C₅ C₆} →
                                    {B' : CategoryTheory.Functor C₄ C₆} →
                                      CategoryTheory.TwoSquare T L R B →
                                        CategoryTheory.TwoSquare T' R R' B' →
                                          CategoryTheory.TwoSquare (T.comp T') L R' (B.comp B')
-- Mathlib.Data.W.Basic
WType.mk : {α : Type u_1} → {β : α → Type u_2} → (a : α) → (β a → WType β) → WType β
-- Init.Data.Array.Lex.Lemmas
Array.empty_lt_push : ∀ {α : Type u_1} [inst : LT α] (xs : Array α) (a : α), #[] < xs.push a
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_singleton_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.colon {0} = ⊤
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map.congr_simp : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F),
  f = f_1 → ∀ (s s_1 : NonUnitalSubring R), s = s_1 → NonUnitalSubring.map f s = NonUnitalSubring.map f_1 s_1
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.subset_verticalStrip_of_isCompact : ∀ {K : Set UpperHalfPlane}, IsCompact K → ∃ A B, 0 < B ∧ K ⊆ UpperHalfPlane.verticalStrip A B
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_univ_ne_zero : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ],
  μ.real Set.univ ≠ 0
-- Mathlib.Topology.Separation.Regular
T4Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X] [toT1Space : T1Space X] [toNormalSpace : NormalSpace X], T4Space X
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.noZeroDivisors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N) [NoZeroDivisors M], NoZeroDivisors N
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.tensorRight'_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b)
  [inst_1 : CategoryTheory.BicategoricalCoherence g (CategoryTheory.CategoryStruct.id b)],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso ≪≫
      CategoryTheory.Bicategory.rightUnitor f
-- Mathlib.Algebra.Lie.InvariantForm
/-- The orthogonal complement of a Lie submodule `N` with respect to an invariant bilinear form `Φ` is
the Lie submodule of elements `y` such that `Φ x y = 0` for all `x ∈ N`.
 -/
LieAlgebra.InvariantForm.orthogonal : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                (Φ : LinearMap.BilinForm R M) →
                  LinearMap.BilinForm.lieInvariant L Φ → LieSubmodule R L M → LieSubmodule R L M
-- Mathlib.Data.Nat.Init
Nat.strongSubRecursion.eq_def : ∀ {P : ℕ → ℕ → Sort u_1} (H : (m n : ℕ) → ((x y : ℕ) → x < m → y < n → P x y) → P m n) (x x_1 : ℕ),
  Nat.strongSubRecursion H x x_1 =
    match x, x_1 with
    | n, m => H n m fun x y x_2 x_3 => Nat.strongSubRecursion H x y
-- Mathlib.Order.LiminfLimsup
/-- The `limsup` of a function `u` along a filter `f` is the infimum of the `a` such that
the inequality `u x ≤ a` eventually holds for `f`.  -/
Filter.limsup : {α : Type u_1} → {β : Type u_2} → [ConditionallyCompleteLattice α] → (β → α) → Filter β → α
-- Init.Data.UInt.Bitwise
instCommutativeUInt32HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.stepAux_write : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (v : σ)
  (a b : Γ) (L R : Turing.ListBlank Γ),
  Turing.TM1.stepAux (Turing.TM1to1.write (enc a).toList q) v
      (Turing.TM1to1.trTape' enc0 L (Turing.ListBlank.cons b R)) =
    Turing.TM1.stepAux q v (Turing.TM1to1.trTape' enc0 (Turing.ListBlank.cons a L) R)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_inter_Ioo_of_right_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  b₂ ≤ b₁ → Set.Ioc a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioo (max a₁ a₂) b₂
-- Init.Data.SInt.Bitwise
ISize.xor_left_inj : ∀ {a b : ISize} (c : ISize), a ^^^ c = b ^^^ c ↔ a = b