mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteBooleanAlgebra
OrderDual.instCompleteDistribLattice : {α : Type u} → [CompleteDistribLattice α] → CompleteDistribLattice αᵒᵈ
-- Init.Data.Range.Polymorphic.UInt
UInt8.upwardEnumerableLE_ofBitVec : ∀ {x y : BitVec 8},
  Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
AlgCat.tensorAlgebraAdj_unit_app : ∀ (R : Type u) [inst : CommRing R] (M : ModuleCat R),
  (AlgCat.tensorAlgebraAdj R).unit.app M = ModuleCat.ofHom (TensorAlgebra.ι R)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Antitone.mul : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] [inst_2 : Preorder α] {f g : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → Antitone g → (∀ (x : α), f x ≤ 0) → (∀ (x : α), g x ≤ 0) → Monotone (f * g)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- The constant-function embedding, as a ring hom.  -/
LocallyConstant.constRingHom : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : NonAssocSemiring Y] → Y →+* LocallyConstant X Y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ofList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {l : List (α × β)},
  (Std.DTreeMap.Raw.Const.ofList l cmp).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Init.Data.BitVec.Lemmas
BitVec.true_cons_zero : ∀ {w : ℕ}, BitVec.cons true 0#w = BitVec.twoPow (w + 1) w
-- Mathlib.Data.Vector.Basic
List.Vector.get_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n), (List.Vector.ofFn f).get i = f i
-- Mathlib.Data.List.Zip
List.revzip_map_snd : ∀ {α : Type u} (l : List α), List.map Prod.snd l.revzip = l.reverse
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.severityHint : Lean.Syntax → Lean.Elab.TermElabM Lean.MessageData
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hom_neg_apply : ∀ {X Y : AddSemigrp} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.go : (pat : String.Slice) →
  (table : Array ℕ) →
    0 < table.size →
      table.size ≤ pat.utf8ByteSize → (∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) → Vector ℕ pat.utf8ByteSize
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_replicateRow : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R] {ι : Type u_11}
  {A : X → n → R}, Continuous A → Continuous fun x => Matrix.replicateRow ι (A x)
-- Init.Data.Option.Array
Option.size_toArray_eq_zero_iff : ∀ {α : Type u_1} {o : Option α}, o.toArray.size = 0 ↔ o = none
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.div.eq_1 : ∀ {R : Type u} [inst : Field R] (p q : Polynomial R),
  p.div q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle : ∀ {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) (i : Fin (n + 1)),
  ↑((s.faceOpposite i).orthogonalProjectionSpan (s.eulerPoint i)) ∈ s.ninePointCircle
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Coalgebra.Repr.tmul_left : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Bialgebra R A] [inst_3 : Semiring B] [inst_4 : Bialgebra R B] {a : A} {b : B}
  (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ) (i : ι × κ),
  (ℛa.tmul ℛb).left i = ℛa.left i.1 ⊗ₜ[R] ℛb.left i.2
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkDecl : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.Order.Defs.PartialOrder
ge_of_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → b ≤ a
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_sInf : ∀ {M : Type u_2} [inst : AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)), (sInf S).unop = sInf (AddSubmonoid.op ⁻¹' S)
-- Lean.Parser.Attr
Lean.Parser.Attr.default_instance.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.hasPullback_unop_iff_hasPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.Limits.HasPullback f.unop g.unop ↔ CategoryTheory.Limits.HasPushout f g
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.facets_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E}, K.facets ⊆ K.faces
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_eq_nil_iff : ∀ {α : Type u} {l : List α}, l.cyclicPermutations = [[]] ↔ l = []
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.degree_completeEquipartiteGraph : ∀ {r t : ℕ} (v : Fin r × Fin t), (SimpleGraph.completeEquipartiteGraph r t).degree v = (r - 1) * t
-- Init.Data.Int.Order
Int.instTransLtLe : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 < x2
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.seminormedAddGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F],
  Prod.seminormedAddGroup =
    { toNorm := Prod.toNorm, toAddGroup := Prod.instAddGroup, toPseudoMetricSpace := Prod.pseudoMetricSpaceMax,
      dist_eq := ⋯ }
-- Init.Data.List.Find
List.IsPrefix.findIdx?_eq_some : ∀ {α : Type u_1} {i : ℕ} {l₁ l₂ : List α} {p : α → Bool},
  l₁ <+: l₂ → List.findIdx? p l₁ = some i → List.findIdx? p l₂ = some i
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.trivial_grp_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_mul_eq_opow_omega0_mul : ∀ {a : Ordinal.{u}}, 0 < a → ∀ (b : Ordinal.{u}), Ordinal.deriv (fun x => a * x) b = a ^ Ordinal.omega0 * b
-- Mathlib.Topology.Connected.PathConnected
pathConnectedSpace_iff_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X], PathConnectedSpace X ↔ IsPathConnected Set.univ
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_sub : ∀ (a b : UInt16), (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 65536
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_sub_eq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  {ab ∈ A ×ˢ B | ab.1 - ab.2 = x}.card = A.addConvolution (-B) x
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesRightKanExtension F L` asserts that `G` preserves all right Kan extensions
of `F` along `L`. See `PreservesRightKanExtension.mk_of_preserves_isRightKanExtension` for a
constructor taking a single right Kan extension as input.  -/
CategoryTheory.Functor.PreservesRightKanExtension : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A B → CategoryTheory.Functor A C → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  Array.find? (fun x => cmp x.1 k == Ordering.eq) t.toArray = none ↔ t.contains k = false
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isAddQuotientCoveringMap_zsmul : ∀ {𝕜 : Type u_1} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)]
  {n : ℤ}, IsUnit ↑n → IsAddQuotientCoveringMap (fun x => n • x) ↥(zsmulAddGroupHom n).ker
-- Mathlib.Data.Sym.Basic
Sym.count_coe_fill_of_ne : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] {a x : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)},
  x ≠ a → Multiset.count x ↑(Sym.fill a i s) = Multiset.count x ↑s
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.inv_one_sub_inv : ∀ {a : ℝ}, 0 < a → a < 1 → a⁻¹.HolderConjugate (1 - a)⁻¹
-- Mathlib.Data.Option.Basic
Option.failure_eq_none : ∀ {α : Type u_5}, failure = none
-- Std.Http.Data.Status
/-- 406 Not Acceptable
 -/
Std.Http.Status.notAcceptable : Std.Http.Status
-- Mathlib.Data.Matrix.Composition
Matrix.compAlgEquiv_symm_apply : ∀ (I : Type u_1) (J : Type u_2) (R : Type u_5) (K : Type u_7) [inst : CommSemiring K] [inst_1 : Semiring R]
  [inst_2 : Fintype I] [inst_3 : Fintype J] [inst_4 : Algebra K R] [inst_5 : DecidableEq I] [inst_6 : DecidableEq J]
  (M : Matrix (I × J) (I × J) R), (Matrix.compAlgEquiv I J R K).symm M = (Matrix.comp I I J J R).symm M
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the infima along a Galois coinsertion  -/
GaloisCoinsertion.liftSemilatticeInf : {α : Type u} →
  {β : Type v} →
    {u : α → β} →
      {l : β → α} → [inst : PartialOrder β] → [inst_1 : SemilatticeInf α] → GaloisCoinsertion l u → SemilatticeInf β
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_add_mul_left : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x, y + z * x} = Ideal.span {x, y}
-- Std.Internal.Do.WP.Conjunctive
/-- `StateT` lifts conjunctivity from its base monad.  -/
Std.Internal.Do.StateT.instWPConjunctive : ∀ {m : Type u → Type v} {σ : Type u} {Pred : Type w} {EPred : Type z} {α : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [Std.Internal.Do.WPConjunctive (m (α × σ)) (α × σ) Pred EPred],
  Std.Internal.Do.WPConjunctive (StateT σ m α) α (σ → Pred) EPred
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_smul : ∀ {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (a : K), a ≠ 0 → (a • f).ker = f.ker
-- Mathlib.Data.Finsupp.Basic
/-- Given a finitely supported function `f` from `α` to the type of
finitely supported functions from `β` to `M`,
`uncurry f` is the "uncurried" finitely supported function from `α × β` to `M`.  -/
Finsupp.uncurry : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Zero M] → (α →₀ β →₀ M) → α × β →₀ M
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.map_app : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (f : B₁.IsometryEquiv B₂) (m n : M₁), (B₂ (f n)) (f m) = (B₁ n) m
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_neg : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeAddGroup α), (-x).toWord = FreeAddGroup.negRev x.toWord
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} [inst_1 : SizeOf C] (I : C) (i₀ i₁ : A ⟶ I) (π : I ⟶ A)
  (i₀_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₀ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam)
  (i₁_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₁ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam),
  sizeOf { I := I, i₀ := i₀, i₁ := i₁, π := π, i₀_π := i₀_π, i₁_π := i₁_π } =
    1 + sizeOf I + sizeOf i₀ + sizeOf i₁ + sizeOf π + sizeOf i₀_π + sizeOf i₁_π
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed version of the mates correspondence.  -/
CategoryTheory.unit_mateEquiv : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : CategoryTheory.TwoSquare G L₁ L₂ H) (c : C),
  CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app c))
      (((CategoryTheory.mateEquiv adj₁ adj₂) α).app (L₁.obj c)) =
    CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj c)))
      (R₂.map (α.app ((CategoryTheory.Functor.id C).obj c)))
-- Mathlib.Topology.CWComplex.Classical.Basic
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.CWComplex.OfDiscreteClosed.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
AddMonoidHom.finsuppSum_apply : ∀ {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [inst : Zero β] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : α →₀ β) (g : α → β → N →+ P) (x : N), (f.sum g) x = f.sum fun i fi => (g i fi) x
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.preservesLimit_comp_of_createsLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.CreatesLimit K F] [CategoryTheory.Limits.PreservesLimit K (F.comp G)],
  CategoryTheory.Limits.PreservesLimit (K.comp F) G
-- Mathlib.Algebra.MonoidAlgebra.Opposite
AddMonoidAlgebra.opRingEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Add M],
  AddMonoidAlgebra.opRingEquiv =
    {
      toEquiv :=
        (MulOpposite.opAddEquiv.symm.trans
            ((AddMonoidAlgebra.mapDomainAddEquiv R AddOpposite.opEquiv).trans
              (AddMonoidAlgebra.mapAddEquiv Mᵃᵒᵖ MulOpposite.opAddEquiv))).toEquiv,
      map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
/-- The natural inclusion from the maximal spectrum to the prime spectrum.  -/
MaximalSpectrum.toPrimeSpectrum : {R : Type u_1} → [inst : CommSemiring R] → MaximalSpectrum R → PrimeSpectrum R
-- Mathlib.Algebra.Star.StarAlgHom
instAlgEquivClassOfNonUnitalAlgEquivClass : ∀ (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : EquivLike F A B]
  [NonUnitalAlgEquivClass F R A B], AlgEquivClass F R A B
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.instEssentiallySmallColimitsCardinalClosureOfLocallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsCardinalClosure κ)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- A `CliffordAlgebra` over a nontrivial ring is nontrivial, in characteristic not two.  -/
CliffordAlgebra.instNontrivialOfInvertibleOfNat : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) [Nontrivial R] [Invertible 2], Nontrivial (CliffordAlgebra Q)
-- Init.Data.SInt.Bitwise
Int64.toInt8_or : ∀ (a b : Int64), (a ||| b).toInt8 = a.toInt8 ||| b.toInt8
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_eq_toNNReal_tsum : ∀ {β : Type u_2} {f : β → NNReal}, ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal
-- Mathlib.Logic.Equiv.Defs
Equiv.conj_trans : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ), (e₁.trans e₂).conj = e₁.conj.trans e₂.conj
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `antitone_toDual_comp_iff`. -/
Monotone.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Antitone (⇑OrderDual.toDual ∘ f)
-- Mathlib.Analysis.SpecificLimits.Basic
lt_geom : ∀ {u : ℕ → ℝ} {c : ℝ}, 0 ≤ c → ∀ {n : ℕ}, 0 < n → (∀ k < n, u (k + 1) < c * u k) → u n < c ^ n * u 0
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.ext : ∀ {α : Type ua} {u₁ u₂ : UniformSpace.Core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
-- Init.Core
/-- `Total X r` means that the binary relation `r` on `X` is total, that is, `r a b` or `r b a`.  -/
Std.Total : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.mk : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] {P : Ideal B}
  {p : Ideal A}, p = Ideal.under A P → P.LiesOver p
-- Mathlib.Logic.Equiv.Multiset
Denumerable.raise_lower : ∀ {l : List ℕ} {n : ℕ}, (n :: l).SortedLE → Denumerable.raise (Denumerable.lower l n) n = l
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Composition of triangle morphisms gives a triangle morphism.
 -/
CategoryTheory.Pretriangulated.TriangleMorphism.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C} →
        CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂ →
          CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃ → CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₃
-- Mathlib.ModelTheory.DirectLimit
/-- The map from a direct limit of a system of substructures of `M` into `M`.  -/
FirstOrder.Language.DirectLimit.liftInclusion : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      [inst_1 : Nonempty ι] →
        [inst_2 : IsDirectedOrder ι] →
          {M : Type u_1} →
            [inst_3 : L.Structure M] →
              (S : ι →o L.Substructure M) →
                L.Embedding
                  (FirstOrder.Language.DirectLimit (fun i => ↥(S i)) fun x x_1 h =>
                    FirstOrder.Language.Substructure.inclusion ⋯)
                  M
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.toOption.eq_1 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {s : String.Slice} (currPos : s.Pos) (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)),
  String.Slice.RevSplitIterator.toOption✝ (String.Slice.RevSplitIterator.operating currPos s_1) = some s_1
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConcaveOn 𝕜 (f '' s) g →
    StrictConcaveOn 𝕜 s f → StrictMonoOn g (f '' s) → Set.InjOn f s → StrictConcaveOn 𝕜 s (g ∘ f)
-- Init.Data.Nat.Lemmas
Nat.div_mul_right_comm : ∀ {a b : ℕ}, b ∣ a → ∀ (c : ℕ), a / b * c = a * c / b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.mul_le_iff_le_one_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : MulOneClass α] [IsMulCommutative α] [MulLeftMono α] {a b : α},
  MulLECancellable a → (b * a ≤ a ↔ b ≤ 1)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The adjunction between the n-skeleton and n-truncation.  -/
CategoryTheory.SimplicialObject.skAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [inst_1 :
          ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] →
        CategoryTheory.SimplicialObject.Truncated.sk n ⊣ CategoryTheory.SimplicialObject.truncation n
-- ProofWidgets.Component.RefreshComponent
/-- A HTML tree together with a version number.
We use this to check whether the tree currently on display is up to date.  -/
ProofWidgets.RefreshComponent.VersionedHtml : Type
-- Lean.DocString.Extension
Lean.addDocStringCore : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → [Lean.MonadEnv m] → [MonadLiftT BaseIO m] → Lean.Name → String → m Unit
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_leftUnitor_hom_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.id
                (Opposite.op
                  (CategoryTheory.Comon.MonOpOpToComonObj
                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                        (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop
        X.X)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p q : P), ((signedDist 0) p) q = 0
-- Mathlib.Data.Fintype.Defs
Finset.subset_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s ⊆ Finset.univ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Return every value that is indexed in the tree.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchEverything : {α : Type} →
  Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex →
    Lean.Meta.RefinedDiscrTree.TreeM✝ α (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The sheaf fibre functor of `point J` is the global sections functor.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.pointSheafFiberIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_5 : CategoryTheory.HasWeakSheafify J A] →
                  (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).sheafFiber ≅ CategoryTheory.Sheaf.Γ J A
-- Std.Time.Format
/-- Parses a `String` in the `AmericanDate` or `SQLDate` format and returns a `PlainDate`.
 -/
Std.Time.PlainDate.parse : String → Except String Std.Time.PlainDate
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_roots : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p ≠ 0 → (a ∈ p.roots ↔ p.IsRoot a)