mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.mk.sizeOf_spec : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] [inst_10 : SizeOf R] [inst_11 : SizeOf S] [inst_12 : SizeOf M]
  [inst_13 : SizeOf M₂] (toLinearEquiv : M ≃ₛₗ[σ] M₂)
  (continuous_toFun : autoParam (Continuous (↑toLinearEquiv).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toLinearEquiv.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam),
  sizeOf
      { toLinearEquiv := toLinearEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    1 + sizeOf toLinearEquiv + sizeOf continuous_toFun + sizeOf continuous_invFun
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.d_apply : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G] {n : ℕ} (f : MonoidAlgebra k (Fin (n + 1 + 1) → G)),
  (Rep.Hom.hom ((Rep.standardComplex k G).d (n + 1) n)) f = (Rep.standardComplex.d k G (n + 1)) f
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.antidiagonal_min_add_min`. -/
Finset.addAntidiagonal_min_mul_min : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty),
  Finset.antidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
-- Mathlib.Data.Int.Order.Basic
Int.mul_nonpos_iff : ∀ {a b : ℤ}, a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters and the letter type ('z' or 'v')
into a `ZoneName` format.
- For 'z', if less than 4 letters, it returns the short form; if 4 letters, it returns the full form.
- For 'v', if 1 letter, it returns the short form; if 4 letters, it returns the full form.
- Otherwise, it returns none.
 -/
Std.Time.ZoneName.classify : Char → ℕ → Option Std.Time.ZoneName
-- Mathlib.Data.Matrix.Basic
/-- This is `Matrix.of` bundled as a linear equivalence.  -/
Matrix.ofLinearEquiv : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_7) →
      {α : Type u_11} →
        [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → (m → n → α) ≃ₗ[R] Matrix m n α
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_restrictLie_incl_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (H : LieSubalgebra R L), LieSubmodule.map (N.incl.restrictLie H) ⊤ = N.restr H
-- Mathlib.Analysis.Oscillation
/-- The oscillation of `f` at `x` is 0 if and only if `f` is continuous at `x`.  -/
Oscillation.eq_zero_iff_continuousAt : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] (f : E → F) (x : E),
  oscillation f x = 0 ↔ ContinuousAt f x
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
measure_Ioc_lt_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α}, μ (Set.Ioc a b) < ⊤
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_option_toFinset : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (o : Option α) (f : α → β),
  ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x
-- Mathlib.Computability.RE
ComputablePred.of_eq : ∀ {α : Type u_1} [inst : Primcodable α] {p q : α → Prop}, ComputablePred p → (∀ (a : α), p a ↔ q a) → ComputablePred q
-- Mathlib.MeasureTheory.Function.Holder
/-- `MeasureTheory.Lp.holder` as a continuous bilinear map.  -/
ContinuousLinearMap.holderL : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        {G : Type u_5} →
          {m : MeasurableSpace α} →
            (μ : MeasureTheory.Measure α) →
              (p q r : ENNReal) →
                [hpqr : p.HolderTriple q r] →
                  [inst : NontriviallyNormedField 𝕜] →
                    [inst_1 : NormedAddCommGroup E] →
                      [inst_2 : NormedAddCommGroup F] →
                        [inst_3 : NormedAddCommGroup G] →
                          [inst_4 : NormedSpace 𝕜 E] →
                            [inst_5 : NormedSpace 𝕜 F] →
                              [inst_6 : NormedSpace 𝕜 G] →
                                (E →L[𝕜] F →L[𝕜] G) →
                                  [inst_7 : Fact (1 ≤ p)] →
                                    [inst_8 : Fact (1 ≤ q)] →
                                      [inst_9 : Fact (1 ≤ r)] →
                                        ↥(MeasureTheory.Lp E p μ) →L[𝕜]
                                          ↥(MeasureTheory.Lp F q μ) →L[𝕜] ↥(MeasureTheory.Lp G r μ)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Ideal.Quotient.liftₐ.congr_simp : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (I : Ideal A) [inst_5 : I.IsTwoSided] (f f_1 : A →ₐ[R₁] B)
  (e_f : f = f_1) (hI : ∀ a ∈ I, f a = 0), Ideal.Quotient.liftₐ I f hI = Ideal.Quotient.liftₐ I f_1 ⋯
-- Mathlib.Order.Monotone.Defs
Monotone.reflect_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {a b : α}, f a < f b → a < b
-- Mathlib.LinearAlgebra.Projection
LinearMap.projectionOnto_of_proj : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  (f : E →ₗ[R] ↥p) (hf : ∀ (x : ↥p), f ↑x = x), p.projectionOnto f.ker ⋯ = f
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.mk.injEq : ∀ (fla : Std.Format.FlattenAllowability) (flb : Std.Format.FlattenBehavior) (items : List Std.Format.WorkItem✝)
  (fla_1 : Std.Format.FlattenAllowability) (flb_1 : Std.Format.FlattenBehavior) (items_1 : List Std.Format.WorkItem✝),
  ({ fla := fla, flb := flb, items := items } = { fla := fla_1, flb := flb_1, items := items_1 }) =
    (fla = fla_1 ∧ flb = flb_1 ∧ items = items_1)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∑' i, f i b`
converges uniformly to `g`, then the sum converges locally uniformly. Note that this is not a
tautology, and the converse is only true if the domain is locally compact.  -/
hasSumLocallyUniformlyOn_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, HasSumUniformlyOn f g t) → HasSumLocallyUniformlyOn f g s
-- Mathlib.Algebra.Torsor.Defs
/-- Adding a group element to the point `p` is an injective
function.  -/
vadd_right_injective : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P), Function.Injective fun x => x +ᵥ p
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Equiv.decidable.match_1.splitter : {α : Type u_1} →
  (motive : Lists α → Lists α → Sort u_2) →
    (x x_1 : Lists α) →
      ((l₁ l₂ : Lists' α false) → motive ⟨false, l₁⟩ ⟨false, l₂⟩) →
        ((l₁ : Lists' α false) → (l₂ : Lists' α true) → motive ⟨false, l₁⟩ ⟨true, l₂⟩) →
          ((l₁ : Lists' α true) → (l₂ : Lists' α false) → motive ⟨true, l₁⟩ ⟨false, l₂⟩) →
            ((l₁ l₂ : Lists' α true) → motive ⟨true, l₁⟩ ⟨true, l₂⟩) → motive x x_1
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_le_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b ↔ ∃ n, |b|ₘ ≤ |a|ₘ ^ n
-- Init.Data.Option.Basic
Option.instDecidableEq : {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.mk.sizeOf_spec : ∀ {α : Type u} [inst : Preorder α] [inst_1 : SizeOf α] (toOrderHom : ℕ →o α),
  sizeOf { toOrderHom := toOrderHom } = 1 + sizeOf toOrderHom
-- Mathlib.Topology.Algebra.MulAction
AddOpposite.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X], ContinuousVAdd M Xᵃᵒᵖ
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- In an `n`-preprimitive action, the action of `fixingSubgroup M s` on `ofFixingSubgroup M s`
is preprimitive, for all sets `s` such that `s.encard + 1 = n`.  -/
MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup : ∀ (M : Type u_1) {α : Type u_2} {inst : Group M} {inst_1 : MulAction M α} (n : ℕ)
  [self : MulAction.IsMultiplyPreprimitive M α n] {s : Set α},
  s.encard + 1 = ↑n → MulAction.IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
-- Lean.Elab.Command
Lean.Elab.Command.instAddErrorMessageContextCommandElabM : Lean.AddErrorMessageContext Lean.Elab.Command.CommandElabM
-- Mathlib.Data.PNat.Xgcd
/-- Final value of `a / d`  -/
PNat.gcdA' : ℕ+ → ℕ+ → ℕ+
-- Mathlib.Data.List.Nodup
Option.toList_nodup : ∀ {α : Type u} (o : Option α), o.toList.Nodup
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumcenter_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).circumcenter = f s.circumcenter
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_morphismRestrict_ι_isoImage_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens),
  CategoryTheory.CategoryStruct.comp (f ∣_ U ∣_ V) (AlgebraicGeometry.Scheme.Hom.isoImage U.ι V).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.isoImage ((TopologicalSpace.Opens.map f.base).obj U).ι
            ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V)).hom
        (X.homOfLE ⋯))
      (f ∣_ (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
-- Init.Data.Nat.Lemmas
Nat.pow_lt_pow_right : ∀ {a m n : ℕ}, 1 < a → m < n → a ^ m < a ^ n
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subsemigroup_strictAnti : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  StrictAnti MulArchimedeanClass.subsemigroup
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.cases'.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin2 n.succ → Sort u_1) (h_1 : Unit → motive Fin2.fz) (h_2 : (n_1 : Fin2 n) → motive n_1.fs),
  (match Fin2.fz with
    | Fin2.fz => h_1 ()
    | n.fs => h_2 n) =
    h_1 ()
-- Mathlib.GroupTheory.Congruence.Defs
Con.toSetoid_top : ∀ {M : Type u_1} [inst : Mul M], ⊤.toSetoid = ⊤
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.left_unitor.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.left_unitor f) = 1 + sizeOf a + sizeOf b + sizeOf f
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.subgroupOrderIsoSubgroupMulChar.eq_1 : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)],
  MulChar.subgroupOrderIsoSubgroupMulChar M R =
    (CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R).trans MulChar.mulEquivToUnitHom.symm.mapSubgroup.dual
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.ofHom_comp : ∀ {R S T : Type u} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] (f : R →+* S) (g : S →+* T),
  SemiRingCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (SemiRingCat.ofHom f) (SemiRingCat.ofHom g)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift_compr₂ₛₗ : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {P₂ : Type u_17} {P₃ : Type u_18} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid P₂]
  [inst_6 : AddCommMonoid P₃] [inst_7 : Module R M] [inst_8 : Module R N] [inst_9 : Module R₂ P₂]
  [inst_10 : Module R₃ P₃] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} [inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (h : P₂ →ₛₗ[σ₂₃] P₃), TensorProduct.lift (f'.compr₂ₛₗ h) = h ∘ₛₗ TensorProduct.lift f'
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
/-- If the sequence with `n`-th term the sup norm of `fun x ↦ f (x + n)` on the interval `Icc 0 1`,
for `n ∈ ℤ`, is summable, then `f` is integrable on `ℝ`.  -/
Real.integrable_of_summable_norm_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(ℝ, E)},
  (Summable fun n => ‖ContinuousMap.restrict (Set.Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖) →
    MeasureTheory.Integrable (⇑f) MeasureTheory.volume
-- Lean.Elab.Tactic.RCases
/-- Like `tryClearMany`, but also clears dependent hypotheses if possible  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.tryClearMany' : Lean.MVarId → Array Lean.FVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Group.Subgroup.Even
Submonoid.square_toSubsemigroup : ∀ {M : Type u_1} [inst : CommMonoid M], (Submonoid.square M).toSubsemigroup = Subsemigroup.square M
-- Mathlib.Algebra.Group.Defs
CommMagma.ext : ∀ {G : Type u} {x y : CommMagma G}, Mul.mul = Mul.mul → x = y
-- Mathlib.Data.Prod.PProd
PProd.exists : ∀ {α : Sort u_1} {β : Sort u_2} {p : α ×' β → Prop}, (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyFun_congr : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s : Set ((i : ι) → α i)} {I : Finset ι}
  {S : Set ((i : ↥I) → α ↑i)},
  MeasureTheory.IsProjectiveMeasureFamily P →
    s ∈ MeasureTheory.measurableCylinders α →
      s = MeasureTheory.cylinder I S → MeasurableSet S → MeasureTheory.projectiveFamilyFun P s = (P I) S
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.ematchTheorems : Lean.PArray Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleType_cycleIcc_of_ge : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → ∀ [NeZero n], (j.cycleIcc i).cycleType = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_of_isLUB : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedMul α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α),
  IsLUB (Set.range fun s => ∏ i ∈ s, f i) b → HasProd f b
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ_σ₀Iter_assoc : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ_σ₀Iter._auto_1),
  autoParam (↑j ≤ i) SimplexCategory.σ_σ₀Iter._auto_3 →
    ∀ {Z : SimplexCategory} (h : { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i hi) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter (i + 1) ⋯) h
-- Lean.Structure
/-- Declares a new structure to the elaborator.
Every structure created by `structure` or `class` has such an entry.
This should be followed up with `setStructureParents` and `setStructureResolutionOrder`.
 -/
Lean.registerStructure : Lean.Environment → Lean.StructureDescr → Lean.Environment
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Key : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [CategoryTheory.CreatesColimits F] → CategoryTheory.CreatesLimits F.op
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- A root, seen as an element of the span of roots.  -/
RootPairing.rootSpanMem : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_6) → [inst_5 : CommRing S] → [inst_6 : Module S M] → ι → ↥(P.rootSpan S)
-- Lean.Parser.Syntax
Lean.Parser.Command.syntaxAbbrev.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restriction_d_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] {i j : ι} {i' j' : ι'} (hi : e.f i = i')
  (hj : e.f j = j'),
  (K.restriction e).d i j =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.restrictionXIso e hj).inv)
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.X.match_1.splitter : {ι : Type u_1} →
  (motive : Option ι → Sort u_2) → (x : Option ι) → ((x : ι) → motive (some x)) → (Unit → motive none) → motive x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ} (it : Std.IterM Id β),
  (Std.IterM.mapWithPostcondition f it).toListRev = List.reverse <$> List.mapM (fun x => (f x).run) it.toList.run
-- Mathlib.Order.Category.PartOrd
/-- The equivalence between `PartOrd` and itself induced by `OrderDual` both ways.  -/
PartOrd.dualEquiv : PartOrd ≌ PartOrd
-- Lean.Compiler.LCNF.Types
/-- `uint64` is a 64-bit unsigned integer.
 -/
Lean.Compiler.LCNF.ImpureType.uint64 : Lean.Expr
-- Lean.Elab.ErrorUtils
/-- Translate numbers (1, 2, 3, 212, 322 ...) to ordinals with appropriate English-language names for
small ordinals (0 through 10 become "zeroth" through "tenth") and postfixes for other numbers
(212 becomes "212th" and 1292 becomes "1292nd").
 -/
_private.Lean.Elab.ErrorUtils.0.Nat.toOrdinal : ℕ → String
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.controlled_of_isUniformEmbedding : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  IsUniformEmbedding f →
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a basemap
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.  -/
Continuous.clm_bundle_apply₂ : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)]
  {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)]
  [inst_19 : TopologicalSpace B] [inst_20 : TopologicalSpace M] [inst_21 : FiberBundle F₁ E₁]
  [inst_22 : VectorBundle 𝕜 F₁ E₁] [inst_23 : FiberBundle F₂ E₂] [inst_24 : VectorBundle 𝕜 F₂ E₂]
  [inst_25 : FiberBundle F₃ E₃] [inst_26 : VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₃ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
  {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)},
  (Continuous fun m => ⟨b m, ψ m⟩) →
    (Continuous fun m => ⟨b m, v m⟩) → (Continuous fun m => ⟨b m, w m⟩) → Continuous fun m => ⟨b m, ((ψ m) (v m)) (w m)⟩
-- Init.Data.Array.Subarray
/-- The underlying array.  -/
Std.Slice.Internal.SubarrayData.array : {α : Type u} → Std.Slice.Internal.SubarrayData α → Array α
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.tail?.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (h : Batteries.PairingHeapImp.Heap α),
  Batteries.PairingHeapImp.Heap.tail? le h = Option.map (fun x => x.2) (Batteries.PairingHeapImp.Heap.deleteMin le h)
-- Lean.Widget.UserWidget
_private.Lean.Widget.UserWidget.0.Lean.Widget.panelWidgetsExt : Lean.Widget.PanelWidgetsExt✝
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on
compacts and inner regular for finite measure sets with respect to compact sets,
they coincide in the following sense: they give the same value to finite measure sets,
up to a multiplicative constant.  -/
MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  [μ.InnerRegularCompactLTTop] [μ'.InnerRegularCompactLTTop] {s : Set G},
  μ s ≠ ⊤ → μ' s ≠ ⊤ → μ' s = μ'.addHaarScalarFactor μ • μ s
-- Mathlib.Data.Multiset.ZeroCons
Multiset.subset_cons : ∀ {α : Type u_1} (s : Multiset α) (a : α), s ⊆ a ::ₘ s
-- Mathlib.Order.OrderIsoNat
WellFoundedGT.ciSup_eq_monotonicSequenceLimit : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] [WellFoundedGT α] (a : ℕ →o α),
  BddAbove (Set.range ⇑a) → iSup ⇑a = monotonicSequenceLimit a
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_eq_self : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y ≤ x → x \ (x \ y) = y
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factorₐ_apply_mk : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (hIJ : I ≤ J) (x : A),
  (Ideal.Quotient.factorₐ R₁ hIJ) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.asFork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X}
  (t : CategoryTheory.IsSplitEqualizer f g h), t.asFork.pt = W
-- Mathlib.Analysis.Complex.RealDeriv
Complex.differentiable_im : Differentiable ℝ Complex.im
-- Mathlib.Topology.Defs.Basic
/-- `IsOpen s` means that `s` is open in the ambient topological space on `X`  -/
IsOpen : {X : Type u} → [TopologicalSpace X] → Set X → Prop