mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Basic
uniformity_addOpposite : ∀ {α : Type ua} [inst : UniformSpace α],
  uniformity αᵃᵒᵖ = Filter.comap (fun q => (AddOpposite.unop q.1, AddOpposite.unop q.2)) (uniformity α)
-- Mathlib.Algebra.Ring.Basic
AddMonoid.End.mulRight_apply_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (y x : R), (AddMonoid.End.mulRight y) x = x * y
-- Mathlib.Data.Seq.Basic
Stream'.Seq.lt_length'_iff : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ}, ↑n < s.length' ↔ ∃ a, a ∈ s.get? n
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.extendCocone_obj_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone (F.comp G)) (X : D),
  (CategoryTheory.Functor.Final.extendCocone.obj c).ι.app X =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.Final.homToLift F X))
      (c.ι.app (CategoryTheory.Functor.Final.lift F X))
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_getLsbD : ∀ {w : ℕ} {x : BitVec w} {i : ℕ}, x.getLsbD i = true → i < w
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `mapConst`, general version.  -/
SatisfiesM.mapConst : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {q : α → Prop} {α_1 : Type u_1} {p : α_1 → Prop} {a : α_1} [inst : Functor m]
  [LawfulFunctor m] {x : m α}, SatisfiesM q x → (∀ {b : α}, q b → p a) → SatisfiesM p (Functor.mapConst a x)
-- Mathlib.Data.Matrix.Basic
/-- For any ring `α`, we have ring isomorphism `Matₙₓₙ(αᵒᵖ) ≅ (Matₙₓₙ(α))ᵒᵖ` given by transpose.

See also `Matrix.transposeRingEquiv` for a version that doesn't take the opposite of `α`,
given that its multiplication is commutative.  -/
RingEquiv.mopMatrix : {m : Type u_2} →
  [inst : Fintype m] →
    {α : Type u_14} → [inst_1 : Mul α] → [inst_2 : AddCommMonoid α] → Matrix m m αᵐᵒᵖ ≃+* (Matrix m m α)ᵐᵒᵖ
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Isomorphic objects have equivalent subobject lattices.  -/
CategoryTheory.Subobject.mapIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : C} → (A ≅ B) → (CategoryTheory.Subobject A ≌ CategoryTheory.Subobject B)
-- Mathlib.Data.Finset.Sups
Finset.sups_inter_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s₁ s₂ t : Finset α},
  (s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.induction : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} {x : α},
  s.WellFoundedOn r → x ∈ s → ∀ {P : α → Prop}, (∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y) → P x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} [inst : SizeOf R] [inst_1 : SizeOf A] (toProd : R × A),
  sizeOf (Unitization.mk toProd) = 1 + sizeOf toProd
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.hom = Y.hom.1
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.isSubterminal_of_terminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.IsSubterminal (⊤_ C)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The section of the augmentation that is induced by the extradegeneracy.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      X.ExtraDegeneracy → ((CategoryTheory.SimplicialObject.const C).obj X.right ⟶ X.left)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.subsingleton_of_subsingleton : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) [Subsingleton M], Subsingleton N
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeOp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F.op ⟶ G.op) (X : C),
  (CategoryTheory.NatTrans.removeOp α).app X = (α.app (Opposite.op X)).unop
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.subset_pointwise_smul_iff : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] {g : G}
  {S T : ValuationSubring K}, S ≤ g • T ↔ g⁻¹ • S ≤ T
-- Mathlib.Geometry.Convex.Cone.Pointed
_private.Mathlib.Geometry.Convex.Cone.Pointed.0.«termR≥0» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.coe_sSup_of_directedOn : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D)
  (F : CategoryTheory.Functor D E)
  [inst_7 : ∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F],
  (J.sheafificationWhiskerLeftIso P).inv.app F = (J.sheafifyCompIso F P).inv
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w) t.fst = h
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_sdiff`. -/
Set.encard_diff : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.Finite → (t \ s).encard = t.encard - s.encard
-- Mathlib.Topology.FiberBundle.Basic
/-- Atlas of a fiber bundle.  -/
FiberBundle.trivializationAtlas : {B : Type u_2} →
  (F : Type u_3) →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        (E : B → Type u_5) →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] →
              [FiberBundle F E] → Set (Bundle.Trivialization F Bundle.TotalSpace.proj)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_sum_univ : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {ι : Type u_3}
  [inst_12 : Fintype ι] (f : ι → R → R) (a : A),
  autoParam (∀ (i : ι), ContinuousOn (f i) (quasispectrum R a)) cfcₙ_sum_univ._auto_1 →
    autoParam (∀ (i : ι), f i 0 = 0) cfcₙ_sum_univ._auto_3 → cfcₙ (∑ i, f i) a = ∑ i, cfcₙ (f i) a
-- Mathlib.SetTheory.ZFC.PSet
PSet.nonempty_type_iff_nonempty : ∀ {x : PSet.{u_1}}, Nonempty x.Type ↔ x.Nonempty
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateIsoEquiv_symm_apply_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (β : r₁ ≅ r₂),
  ((CategoryTheory.Bicategory.conjugateIsoEquiv adj₁ adj₂).symm β).inv =
    (CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₁).symm β.inv
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.uri : Lean.Lsp.LeanModule → Lean.Lsp.DocumentUri
-- Std.Http.Server
/-- The local socket address the server is bound to. When `serve` is called with a port of `0`, this
reflects the ephemeral port assigned by the OS rather than the requested address.
`none` for servers constructed without an associated listening socket (e.g. `serveConnection`).
 -/
Std.Http.Server.localAddr : Std.Http.Server → Option Std.Net.SocketAddress
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.Algebra.Group.Action.Pi
Pi.vadd_apply' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} (i : ι) [inst : (i : ι) → VAdd (α i) (β i)] (s : (i : ι) → α i)
  (x : (i : ι) → β i), (s +ᵥ x) i = s i +ᵥ x i
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Construct a cone over a wide cospan.  -/
CategoryTheory.Limits.WidePullbackShape.mkCone : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} →
        {X : C} →
          (f : X ⟶ F.obj none) →
            (π : (j : J) → X ⟶ F.obj (some j)) →
              (∀ (j : J),
                  CategoryTheory.CategoryStruct.comp (π j)
                      (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) =
                    f) →
                CategoryTheory.Limits.Cone F
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetInstance.toWidgetInstance : Lean.Widget.PanelWidgetInstance → Lean.Widget.WidgetInstance
-- Std.Data.TreeSet.Basic
/-- Returns the `n`-th smallest element, or panics if `n` is at least `t.size`.  -/
Std.TreeSet.atIdx! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → ℕ → α
-- Mathlib.Algebra.Homology.Homotopy
prevD_eq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) {j j' : ι},
  c.Rel j' j → (prevD j) f = CategoryTheory.CategoryStruct.comp (f j j') (D.d j' j)
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.hName? : Lean.Meta.GeneralizeArg → Option Lean.Name
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- If `M` is `R`-free, its rank at stalks is constant and agrees with the `R`-rank of `M`.  -/
Module.rankAtStalk_eq_finrank_of_free : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M],
  Module.rankAtStalk M = ↑(Module.finrank R M)
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobenius_frobeniusRotation : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
  WittVector.frobenius (WittVector.frobeniusRotation p ha₁ ha₂) * a₁ = WittVector.frobeniusRotation p ha₁ ha₂ * a₂
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsNatCastApply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁], IsNatCastApply (M₁ →L[R₁] M₁) M₁
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Notation for the vertical composition of 2-squares.  -/
CategoryTheory.TwoSquare.«term_≫ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.localizationAway.congr_simp : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r r_1 : R) (e_r : r = r_1)
  [inst_3 : IsLocalization.Away r S],
  Algebra.Presentation.localizationAway S r = Algebra.Presentation.localizationAway S r_1
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_trans : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b c : α},
  Std.PRange.UpwardEnumerable.LE a b → Std.PRange.UpwardEnumerable.LE b c → Std.PRange.UpwardEnumerable.LE a c
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.instAddCommGroupR : (σ K : Type u) → [inst : Fintype K] → [inst_1 : CommRing K] → AddCommGroup (MvPolynomial.R σ K)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.kind : Lean.Environment.AddConstAsyncResult → Lean.ConstantKind
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.instCompleteSpace : ∀ {α : Type u_1} [inst : UniformSpace α] [CompleteSpace α], CompleteSpace (TopologicalSpace.Compacts α)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.finrank_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V},
  B.Nondegenerate → ∀ (W : Submodule K V), Module.finrank K ↥(B.orthogonal W) = Module.finrank K V - Module.finrank K ↥W
-- Init.Data.Int.OfNat
Nat.ToInt.lt_eq : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → (a < b) = (a' < b')
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
MonotoneOn.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, MonotoneOn f s → AntitoneOn (fun x => -f x) s
-- Mathlib.LinearAlgebra.Reflection
/-- Composite of reflections in "parallel" hyperplanes is a shear (special case).  -/
Module.reflection_reflection_iterate : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} {y : M} {g : Module.Dual R M} (hfx : f x = 2) (hgy : g y = 2),
  f y * g x = 4 → ∀ (n : ℕ), (⇑(Module.reflection hgy ≪≫ₗ Module.reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimTargetView.mk.injEq : ∀ (hIdent? : Option Lean.Ident) (term : Lean.Syntax) (hIdent?_1 : Option Lean.Ident) (term_1 : Lean.Syntax),
  ({ hIdent? := hIdent?, term := term } = { hIdent? := hIdent?_1, term := term_1 }) =
    (hIdent? = hIdent?_1 ∧ term = term_1)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnRingHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring Y] (a : LocallyConstant X Y) (a_1 : X),
  LocallyConstant.coeFnRingHom a a_1 = a a_1
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment.eq_2 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.hasNegAssignment = true
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.isUnfoldReducibleTarget : Lean.Expr → Lean.CoreM Bool
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_uIcc : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.map (Fin.castLEEmb h) (Finset.uIcc a b) = Finset.uIcc (Fin.castLE h a) (Fin.castLE h b)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendRestrictScalarsAdj_homEquiv_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {M : ModuleCat R}
  {N : ModuleCat S} (φ : (ModuleCat.extendScalars f).obj M ⟶ N) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (((ModuleCat.extendRestrictScalarsAdj f).homEquiv M N) φ)) m =
    (CategoryTheory.ConcreteCategory.hom φ) (1 ⊗ₜ[R] m)
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsOpenEmbedding.functor.congr_simp : ∀ {X Y : TopCat} {f f_1 : X ⟶ Y} (e_f : f = f_1)
  (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)), hf.functor = ⋯.functor
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.map_empty_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [inst : AddCancelMonoid β]
  {T : Set α → β}, MeasureTheory.FinMeasAdditive μ T → T ∅ = 0
-- Init.Data.Fin.Bitwise
Fin.or_val_of_uInt64Size : ∀ (a b : Fin UInt64.size), ↑(a ||| b) = ↑a ||| ↑b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- The "inclusion" maps to the colimit module, as an additive map.  -/
PresheafOfModules.ModuleColimit.ιM : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {cR : CategoryTheory.Limits.Cocone R} →
        {hcR : CategoryTheory.Limits.IsColimit cR} →
          {M : PresheafOfModules R} →
            {cM : CategoryTheory.Limits.Cocone M.presheaf} →
              {hcM : CategoryTheory.Limits.IsColimit cM} →
                {U : Cᵒᵖ} → ↑(M.obj U) →+ PresheafOfModules.ModuleColimit hcR hcM
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.divSubtractShift.match_1.eq_1 : ∀ {w : ℕ} (motive : BitVec.DivModArgs w → Sort u_1) (n d : BitVec w)
  (h_1 : (n d : BitVec w) → motive { n := n, d := d }),
  (match { n := n, d := d } with
    | { n := n, d := d } => h_1 n d) =
    h_1 n d
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.mu_eq_mu' : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α], IncidenceAlgebra.mu 𝕜 = IncidenceAlgebra.mu'✝ 𝕜
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The transpose of a matrix.

This is available in bundled forms as:
* `Matrix.transposeAddEquiv`
* `Matrix.transposeLinearEquiv`
* `Matrix.transposeRingEquiv`
* `Matrix.transposeAlgEquiv`
* `RingEquiv.mopMatrix`
* `AlgEquiv.mopMatrix`
 -/
Matrix.transpose : {m : Type u_2} → {n : Type u_3} → {α : Type v} → Matrix m n α → Matrix n m α
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.lt_iff_lex_lt : ∀ {I : Type u} [inst : LinearOrder I] (l m : Profinite.NobelingProof.Products I),
  l < m ↔ List.Lex (fun x1 x2 => x1 < x2) ↑l ↑m
-- Std.Http.Data.URI.Basic
Std.Http.URI.Query.instInsertProdString : Insert (String × String) Std.Http.URI.Query
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getFirstAltLhs : Lean.Syntax → Lean.Syntax
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The closed unit ball of a valued ring is closed.  -/
Valued.isClosed_integer : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  IsClosed ↑Valued.v.integer
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.ne_top : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsMaximal → I ≠ ⊤
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.getOnlyExtensionState : Lean.MetaM Lean.Meta.Grind.ExtensionState
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.algebraMap_mem_map_algebraMap_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (I : Ideal R) (x : R),
  (algebraMap R S) x ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocCommRing.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocCommRing R},
  inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.pushAtomString : Lean.PrettyPrinter.Formatter
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF → (m.alter k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f m[k]?).isNone)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) {v : NumberField.InfinitePlace K} [w.LiesOver v]
  [inst_4 : Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion]
  [ContinuousSMul v.Completion w.Completion],
  v.IsReal →
    NumberField.ComplexEmbedding.LiesOver (NumberField.InfinitePlace.Completion.extensionEmbedding w)
      (NumberField.InfinitePlace.Completion.extensionEmbedding v)
-- Lean.Elab.Command
Lean.Elab.Command.getMainModule : Lean.Elab.Command.CommandElabM Lean.Name
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- Map from `lpMeasSubgroup` to `Lp F p (μ.trim hm)`.  -/
MeasureTheory.lpMeasSubgroupToLpTrim : {α : Type u_1} →
  (F : Type u_2) →
    (p : ENNReal) →
      [inst : NormedAddCommGroup F] →
        {m m0 : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) →
            (hm : m ≤ m0) → ↥(MeasureTheory.lpMeasSubgroup F m p μ) → ↥(MeasureTheory.Lp F p (μ.trim hm))
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).hom = Y.hom.2
-- Init.GrindInstances.Ring.Nat
Lean.Grind.instIsCharPNatOfNat : Lean.Grind.IsCharP ℕ 0
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.rightInverse_of_injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.LeftInverse f g → Function.Injective f → Function.RightInverse f g
-- Init.Data.SInt.Lemmas
Int64.div_one : ∀ {a : Int64}, a / 1 = a
-- Mathlib.Analysis.MeanInequalities
/-- The `L_p` seminorm of a vector `f` is the greatest value of the inner product
`∑ i ∈ s, f i * g i` over functions `g` of `L_q` seminorm less than or equal to one.  -/
NNReal.isGreatest_Lp : ∀ {ι : Type u} (s : Finset ι) (f : ι → NNReal) {p q : ℝ},
  p.HolderConjugate q →
    IsGreatest ((fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}) ((∑ i ∈ s, f i ^ p) ^ (1 / p))
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Curries an `(M ⊕ N)`-cube into an `M`-cube of `N`-cubes.  -/
GenLoop.currySum : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {M : Type u_3} → (x : X) → ↑(GenLoop (M ⊕ N) X x) → C(M → ↑unitInterval, ↑(GenLoop N X x))
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_image_le : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (W : (↑U).Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj W ≤ U
-- Mathlib.Data.Sigma.Basic
Prod.fst_toSigma : ∀ {α : Type u_7} {β : Type u_8} (x : α × β), x.toSigma.fst = x.1
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.eq_iso_hom : ∀ (f : CategoryTheory.WalkingIso.zero ⟶ CategoryTheory.WalkingIso.one), f = CategoryTheory.WalkingIso.iso.hom
-- Mathlib.Data.Num.ZNum
ZNum.gcd_to_nat : ∀ (a b : ZNum), ↑(a.gcd b) = (↑a).gcd ↑b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_le_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km kmi : α},
  t.max? = some km → (t.insert k).max?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.RingObjCat C} {f g : R₁ ⟶ R₂},
  f.hom = g.hom → f = g