mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Seminormed commutative ring structure on the product of two seminormed commutative rings,
using the sup norm.  -/
Prod.seminormedCommRing : {α : Type u_2} → {β : Type u_3} → [SeminormedCommRing α] → [SeminormedCommRing β] → SeminormedCommRing (α × β)
-- Mathlib.Algebra.Group.Defs
/-- Multiplication by an integer.
Set this to `zsmulRec` unless `Module` diamonds are possible.  -/
ZSMul.zsmul : {G : Type u} → [self : ZSMul G] → ℤ → G → G
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- A function in `Lp` can be approximated in `Lp` by continuous functions.  -/
MeasureTheory.Lp.boundedContinuousFunction_dense : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [inst_3 : BorelSpace α]
  (E : Type u_2) [inst_4 : NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [NormedSpace ℝ E]
  [inst_6 : SecondCountableTopologyEither α E] [inst_7 : Fact (1 ≤ p)],
  p ≠ ⊤ → ∀ [μ.WeaklyRegular], Dense ↑(MeasureTheory.Lp.boundedContinuousFunction E p μ)
-- Mathlib.Order.Category.HeytAlg
HeytAlg.coe_id : ∀ {X : HeytAlg}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuous_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {z : β},
  LowerSemicontinuous fun _x => z
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- A version of **Markov's inequality** with elements of Lp.  -/
MeasureTheory.Lp.meas_ge_le_mul_pow_enorm : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)),
  p ≠ 0 → p ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → μ {x | ε ≤ ↑‖↑↑f x‖₊} ≤ ε⁻¹ ^ p.toReal * ENNReal.ofReal ‖f‖ ^ p.toReal
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.induction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C)
  {P : {a b : CategoryTheory.Quotient r} → (a ⟶ b) → Prop},
  (∀ {x y : C} (f : x ⟶ y), P ((CategoryTheory.Quotient.functor r).map f)) →
    ∀ {a b : CategoryTheory.Quotient r} (f : a ⟶ b), P f
-- Init.Data.FloatArray.Basic
FloatArray.get? : FloatArray → ℕ → Option Float
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The exponent of a generalized eigenvalue is never 0.  -/
Module.End.HasUnifEigenvalue.exp_ne_zero : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, f.HasUnifEigenvalue μ ↑k → k ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_id_comp_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) {l₂ : c ⟶ d} {r₂ : d ⟶ c}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {f : a ⟶ c} {g : b ⟶ d}
  (φ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) l₂) ⟶
      CategoryTheory.CategoryStruct.comp l₁ g),
  (CategoryTheory.Bicategory.mateEquiv adj₁ ((CategoryTheory.Bicategory.Adjunction.id c).comp adj₂)) φ =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor l₂).inv) φ))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp g r₂)).inv
        (CategoryTheory.Bicategory.associator g r₂ (CategoryTheory.CategoryStruct.id c)).hom)
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.sup : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → Max { P // IsLprojection X P }
-- Mathlib.Data.Fintype.Perm
mem_of_mem_permsOfList : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {f : Equiv.Perm α}, f ∈ permsOfList l → ∀ {x : α}, f x ≠ x → x ∈ l
-- Init.Data.SInt.Lemmas
Int16.toInt32_div_of_ne_right : ∀ (a b : Int16), b ≠ -1 → (a / b).toInt32 = a.toInt32 / b.toInt32
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.takeEndWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.takeEndWhile pat = s.sliceFrom (s.skipSuffixWhile pat)
-- Lean.Elab.Tactic.Try
/-- Erases from `tacss` tactics occurring in `tacs`.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.eraseTacs : Array (Array (Lean.TSyntax `tactic)) → Array (Lean.TSyntax `tactic) → Array (Array (Lean.TSyntax `tactic))
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A simple graph contains its subgraphs.  -/
SimpleGraph.IsContained.of_le : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V}, G₁ ≤ G₂ → G₁.IsContained G₂
-- Init.Data.UInt.Basic
instAndOpUInt64 : AndOp UInt64
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.zsmul : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s : Set α}, s.Nonempty → ∀ {n : ℤ}, (n • s).Nonempty
-- Mathlib.NumberTheory.MulChar.Basic
/-- This is the corresponding extension of `MonoidHomClass`.  -/
MulCharClass : (F : Type u_3) →
  (R : outParam (Type u_4)) →
    (R' : outParam (Type u_5)) → [CommMonoid R] → [CommMonoidWithZero R'] → [FunLike F R R'] → Prop
-- Lean.DocString.Parser
/-- Like `satisfyFn`, but no special handling of EOI  -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.satisfyFn' : (Char → Bool) → optParam String "unexpected character" → Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddZeroClass.eq_1 : ∀ {α : Type u_1} [inst : AddZeroClass α],
  Lex.instAddZeroClass = { toZero := Lex.instZero, toAdd := Lex.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toArray_rcc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...=n).toArray[i]?.isSome = true) = (i < (n + 1 - m).toNat)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- The class group of `R` is isomorphic to the group of invertible `R`-submodules in `Frac(R)`
modulo the principal submodules (invertible submodules are automatically fractional ideals).  -/
ClassGroup.mulEquivUnitsSubmoduleQuotRange : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      ClassGroup R ≃* (Submodule R (FractionRing R))ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).range
-- Aesop.Builder.Cases
Aesop.RuleBuilderOptions.casesTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.mul_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (b : M), ContinuousOn (fun x => f x * b) s
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_bijective : ∀ {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] [Module.Finite R M] [Module.Projective R M],
  Function.Bijective ⇑(dualTensorHom R M N)
-- Lean.Language.Basic
/-- Creates diagnostics from a single error message that should span the whole file.  -/
Lean.Language.diagnosticsOfHeaderError : String → Lean.Language.ProcessingM Lean.Language.Snapshot.Diagnostics
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.succ.match_1.eq_3 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit1)
  (h_3 : (n : PosNum) → motive n.bit0),
  (match n.bit0 with
    | PosNum.one => h_1 ()
    | n.bit1 => h_2 n
    | n.bit0 => h_3 n) =
    h_3 n
-- Mathlib.Util.FormatTable
/-- Render a two-dimensional array of `String`s into a markdown-compliant table.
`headers` is a list of column headers,
`table` is a 2D array of cell contents,
`alignments` describes how to align each table column (default: left-aligned).  -/
formatTable : Array String → Array (Array String) → optParam (Option (Array Alignment)) none → String
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- The product of two circulant matrices `circulant v` and `circulant w` is
the circulant matrix generated by `circulant v *ᵥ w`.  -/
Matrix.circulant_mul : ∀ {α : Type u_1} {n : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : AddGroup n]
  (v w : n → α), Matrix.circulant v * Matrix.circulant w = Matrix.circulant ((Matrix.circulant v).mulVec w)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.equiv` as a uniform isomorphism.  -/
WithLp.uniformEquivProd : (p : ENNReal) →
  (α : Type u_2) → (β : Type u_3) → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → WithLp p (α × β) ≃ᵤ α × β
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.coe_of_s_get?_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ},
  v = ↑q →
    ∀ (n : ℕ), Option.map (GenContFract.Pair.map Rat.cast) ((GenContFract.of q).s.get? n) = (GenContFract.of v).s.get? n
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.HasInjectiveResolutions.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.HasInjectiveResolutions C = CategoryTheory.HasInjectiveResolutions C
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_eq_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) {x y : M × ↥S},
  (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 + ↑y.2) = g (y.1 + ↑x.2)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_le_compl : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, s.compl ≤ t.compl ↔ s ≤ t
-- Mathlib.GroupTheory.Coset.Basic
/-- An additive group is made up of a disjoint union of cosets of an additive
subgroup.  -/
QuotientAddGroup.univ_eq_iUnion_vadd : ∀ {α : Type u_1} [inst : AddGroup α] (H : AddSubgroup α), Set.univ = ⋃ x, Quotient.out x +ᵥ ↑H
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] (c c' : Cᵒᵖ) (d : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.unop c) (Opposite.unop c')
      (Opposite.unop d) =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).symm.unop
-- Mathlib.Topology.Order.Compact
/-- This typeclass says that all closed intervals in `α` are compact. This is true for all
conditionally complete linear orders with order topology and products (finite or infinite)
of such spaces.  -/
CompactIccSpace : (α : Type u_1) → [TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.unop_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ Dᵒᵖ), e.unop.functor = e.functor.unop
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addLeftCancelSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddLeftCancelSemigroup (f i)],
  Pi.addLeftCancelSemigroup = { toAddSemigroup := Pi.addSemigroup, toIsLeftCancelAdd := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDHashMap.ofList l).getKeyD k fallback = fallback
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_nonneg : ∀ {a : ℤ}, 0 ≤ a → ∀ (b : ℕ), 0 ≤ mkRat a b
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rii.count_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {r : Std.Rii α},
  r.iter.length = r.size
-- Lean.Meta.Basic
Lean.Meta.Config.toConfigWithKey : Lean.Meta.Config → Lean.Meta.ConfigWithKey
-- Init.Omega.Int
Lean.Omega.Fin.le_of_not_lt : ∀ {n : ℕ} {i j : Fin n}, ¬i < j → j ≤ i
-- Mathlib.RingTheory.LaurentSeries
/-- The prime ideal `(X)` of `K⟦X⟧`, when `K` is a field, as a term of the `HeightOneSpectrum`.  -/
PowerSeries.idealX : (K : Type u_2) → [inst : Field K] → IsDedekindDomain.HeightOneSpectrum (PowerSeries K)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.add_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  (f g : BoxIntegral.BoxAdditiveMap ι M I₀) (J : BoxIntegral.Box ι), (f + g) J = f J + g J
-- Mathlib.Analysis.Normed.Affine.MazurUlam
/-- A bijective isometry sends midpoints to midpoints.  -/
IsometryEquiv.map_midpoint : ∀ {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : MetricSpace PE] [inst_3 : NormedAddTorsor E PE] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F]
  [inst_6 : MetricSpace PF] [inst_7 : NormedAddTorsor F PF] (f : PE ≃ᵢ PF) (x y : PE),
  f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forIn_eq_forIn : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Raw.forIn f init t = forIn t init fun a b => f a.fst a.snd b
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.mk.sizeOf_spec : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] [inst_4 : SizeOf R] [inst_5 : SizeOf E] [inst_6 : SizeOf F]
  (toFourierTransformInv : FourierTransformInv E F)
  (fourierInv_add :
    ∀ (f g : E),
      FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g)
  (fourierInv_smul : ∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f),
  sizeOf
      { toFourierTransformInv := toFourierTransformInv, fourierInv_add := fourierInv_add,
        fourierInv_smul := fourierInv_smul } =
    1 + sizeOf toFourierTransformInv
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- A probability mass function, or discrete probability measures is a function `α → ℝ≥0∞` such
that the values have (infinite) sum `1`.  -/
PMF : Type u → Type u
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_le_pi : ∀ (x : ℂ), x.arg ≤ Real.pi
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts_supportsStmt : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : Inhabited Λ] {M : Λ → Turing.TM2.Stmt Γ Λ σ}
  {S : Finset Λ} {q : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2.Supports M S → some q ∈ Turing.TM2.stmts M S → Turing.TM2.SupportsStmt S q
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.card_filter_eigenvalues_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (μ : 𝕜),
  {i | ↑(hT.eigenvalues hn i) = μ}.card = Module.finrank 𝕜 ↥(Module.End.eigenspace T μ)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.ext_iff : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {w₁ w₂ : Monoid.PushoutI.NormalWord d},
  w₁ = w₂ ↔ w₁.head = w₂.head ∧ w₁.toList = w₂.toList
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.nhds_coe_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), nhds ↑x = Filter.map OnePoint.some (nhds x)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.cocycle_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i j k : self.J) {Z : C}
  (h : CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.t' i j k)
      (CategoryTheory.CategoryStruct.comp (self.t' j k i) (CategoryTheory.CategoryStruct.comp (self.t' k i j) h)) =
    h
-- Init.Data.Option.Basic
Option.join_none : ∀ {α : Type u_1}, none.join = none
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.WithInitial Cᵒᵖ} (f : x ⟶ y),
  (CategoryTheory.WithTerminal.opEquiv C).inverse.map f =
    match x, y, f with
    | CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f =>
      CategoryTheory.WithInitial.down f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x =>
      Opposite.op (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of unop))
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x =>
      CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithTerminal.star)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.Subtype.separatesPoints : ∀ {α : Type u_1} [inst : MeasurableSpace α] [h : MeasurableSpace.SeparatesPoints α] {s : Set α},
  MeasurableSpace.SeparatesPoints ↑s
-- Init.Data.UInt.Bitwise
UInt64.ofNatLT_xor : ∀ (a b : ℕ) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64),
  UInt64.ofNatLT (a ^^^ b) ⋯ = UInt64.ofNatLT a ha ^^^ UInt64.ofNatLT b hb
-- Mathlib.RingTheory.Flat.Rank
CommRingCat.finrank_eq_of_isPushout : ∀ {R S T P : CommRingCat} {f : R ⟶ S} {g : R ⟶ T} {inl : S ⟶ P} {inr : T ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    (CommRingCat.Hom.hom f).Flat →
      (CommRingCat.Hom.hom f).Finite →
        ∀ (x : PrimeSpectrum ↑T),
          (CommRingCat.Hom.hom inr).finrank x =
            (CommRingCat.Hom.hom f).finrank (PrimeSpectrum.comap (CommRingCat.Hom.hom g) x)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- If all elements of a nonempty set `s` are less than or equal to all elements
of a nonempty set `t`, then there exists an element between these sets.  -/
exists_between_of_forall_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  s.Nonempty → t.Nonempty → (∀ x ∈ s, ∀ y ∈ t, x ≤ y) → (upperBounds s ∩ lowerBounds t).Nonempty
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- If `P : MorphismProperty C` is such that any object in `C` maps to the
target of some morphism in `P`, then `P.pushouts` contains the isomorphisms.  -/
CategoryTheory.MorphismProperty.isomorphisms_le_pushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  (∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, CategoryTheory.IsIso p) →
    CategoryTheory.MorphismProperty.isomorphisms C ≤ P.pushouts
-- Mathlib.Algebra.Order.Hom.Monoid
/-- The identity map as an ordered additive monoid isomorphism.  -/
OrderAddMonoidIso.refl : (α : Type u_2) → [inst : Preorder α] → [inst_1 : Add α] → α ≃+o α
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.isCycle : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.IsThreeCycle → σ.IsCycle
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.takeFirst? : {α : Type u_1} → Array α → Option (α × Array α)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.neg_one_lt_zero : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R], -1 < 0
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.createsLimitsOfSize : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {T : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} T] →
        {X : T} →
          {G : CategoryTheory.Functor A T} →
            [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] →
              CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₁, max u₁ v₃, u₁}
                (CategoryTheory.StructuredArrow.proj X G)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_inf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f →
    ∀ (S T : AddSubmonoid N), AddSubmonoid.map f (AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T) = S ⊓ T
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue.val : (self : Lean.Meta.Sym.BitVecValue) → BitVec self.n
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- A Hilbert space is a complete normed inner product space.  -/
HilbertSpace : (𝕜 : Type u_4) →
  (E : Type u_5) →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → [CompleteSpace E] → Type
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.shift_app_comm : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
          ((CategoryTheory.shiftFunctor D a).map (τ.app X)) =
        CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
          ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_mul_two : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) 2
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.limit_mon_one : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.MonObj.one =
    hc.lift
      { pt := CategoryTheory.MonoidalCategoryStruct.tensorUnit C,
        π := { app := fun X => CategoryTheory.MonObj.one, naturality := ⋯ } }
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) (a : α), (f.comp g) a = f (g a)
-- Std.Http.Data.Chunk
/-- Optional metadata associated with this chunk as key-value pairs. Keys are validated
`Chunk.ExtensionName` values, values are optional strings.
 -/
Std.Http.Chunk.extensions : Std.Http.Chunk → Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)