mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.vcomp.injEq : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} {f g h : a ⟶ b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) (g_1 : a ⟶ b)
  (η_1 : CategoryTheory.FreeBicategory.Hom₂ f g_1) (θ_1 : CategoryTheory.FreeBicategory.Hom₂ g_1 h),
  (η.vcomp θ = η_1.vcomp θ_1) = (g = g_1 ∧ η ≍ η_1 ∧ θ ≍ θ_1)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- If a block has too many translates, then it is a (sub)singleton  -/
MulAction.IsBlock.subsingleton_of_card_lt : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {B : Set X}
  [Finite X], MulAction.IsBlock G B → Nat.card X < 2 * (MulAction.orbit G B).ncard → B.Subsingleton
-- Init.Data.UInt.Lemmas
UInt32.neg_sub : ∀ {a b : UInt32}, -(a - b) = b - a
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminormAux_add_le : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] (p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))),
  PiTensorProduct.projectiveSeminormAux (p + q) ≤
    PiTensorProduct.projectiveSeminormAux p + PiTensorProduct.projectiveSeminormAux q
-- Mathlib.Algebra.Central.End
Module.End.mem_subalgebraCenter_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : CommSemiring S] [inst_5 : Module S M] [inst_6 : SMulCommClass R S M]
  [inst_7 : Algebra S R] [inst_8 : IsScalarTower S R M] {f : Module.End R M},
  f ∈ Subalgebra.center S (Module.End R M) ↔ ∃ α, ∃ (hα : α ∈ Subalgebra.center S R), f = Module.End.smulLeft α hα
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.eq_span_root : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [NeZero 2] [inst_4 : Module K M] [inst_5 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  (q : ↥P.invtRootSubmodule), ↑q = Submodule.span K (⇑P.root '' {i | P.root i ∈ ↑q})
-- Lean.Elab.MutualInductive
Lean.Elab.Command.CtorView.mk : Lean.Syntax →
  Lean.Elab.Modifiers → Lean.Name → Lean.Syntax → Lean.Syntax → Option Lean.Syntax → Lean.Elab.Command.CtorView
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankExtends.below_of_le : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {l l₁ l₂ : List Γ},
  Turing.BlankExtends l l₁ → Turing.BlankExtends l l₂ → l₁.length ≤ l₂.length → Turing.BlankExtends l₁ l₂
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.singleObjXIsoOfEq.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : V) (i : ι) (hi : i = j),
  HomologicalComplex.singleObjXIsoOfEq c j A i hi = HomologicalComplex.singleObjXIsoOfEq c j A i hi
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.Const.alterKey : {α : Type u} → {β : Type v} → [BEq α] → α → (Option β → Option β) → List ((_ : α) × β) → List ((_ : α) × β)
-- Init.Data.Array.Lemmas
Array.prod_toList : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] {as : Array α}, as.toList.prod = as.prod
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.gMul_eq_coe_linearMap : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (a : TensorPower R i M) (b : TensorPower R j M),
  GradedMonoid.GMul.mul a b =
    (((TensorProduct.mk R (TensorPower R i M) (TensorPower R j M)).compr₂ ↑TensorPower.mulEquiv) a) b
-- Mathlib.Algebra.Group.Basic
div_mul_mul_cancel : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), a / c * (b * c) = a * b
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.of_equiv_equiv : ∀ {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [inst : Field A₁] [inst_1 : Ring B₁]
  [inst_2 : Field A₂] [inst_3 : Ring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) → ∀ [Algebra.IsSeparable A₁ B₁], Algebra.IsSeparable A₂ B₂
-- Init.Data.List.Basic
List.leftpad.eq_1 : ∀ {α : Type u} (n : ℕ) (a : α) (l : List α), List.leftpad n a l = List.replicate (n - l.length) a ++ l
-- Init.Data.List.BasicAux
/-- Applies a monadic function to each element of a list, returning the list of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new list if the result of each function call is
pointer-equal to its argument.
 -/
List.mapMonoM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → List α → (α → m α) → m (List α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
          k ∈ List.map Sigma.fst toInsert →
            Std.Internal.List.getKeyD k' (Std.Internal.List.insertList l toInsert) fallback = k
-- Mathlib.Data.Num.Lemmas
PosNum.addCommSemigroup : AddCommSemigroup PosNum
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of additive monoid homomorphisms is associative.  -/
ZeroHom.comp_assoc : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
  [inst_3 : Zero Q] (f : ZeroHom M N) (g : ZeroHom N P) (h : ZeroHom P Q), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.add` -/
DifferentiableOn.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 g s → DifferentiableOn 𝕜 (fun i => f i + g i) s
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.mconv_withDensity_eq_mlconvolution₀ : ∀ {G : Type u_3} [inst : Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant] {f g : G → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ → (μ.withDensity f).mconv (μ.withDensity g) = μ.withDensity (MeasureTheory.mlconvolution f g μ)
-- Init.Data.Range.Polymorphic.Fin
Fin.pRangeSucc?_eq : ∀ {n : ℕ}, Std.PRange.succ? = fun x => x.addNat? 1
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.braiding_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.braiding Y).inv.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_split_cert.eq_1 : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly), Lean.Grind.Linarith.diseq_split_cert p₁ p₂ = (p₂ == p₁.mul (-1))
-- Mathlib.Algebra.Group.Hom.Defs
map_ne_one_iff : ∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : One R] [inst_1 : One S] [inst_2 : FunLike F R S]
  [OneHomClass F R S] (f : F), Function.Injective ⇑f → ∀ {x : R}, f x ≠ 1 ↔ x ≠ 1
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ForwardPattern.dropPrefix? : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → (s : String.Slice) → Option s.Pos
-- Mathlib.Data.Nat.Init
/-- **Alias** of `Nat.strongRec`. -/
Nat.strongRec' : {motive : ℕ → Sort u_1} → ((n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) → (t : ℕ) → motive t
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldMap_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.CategoryStruct.comp f g) x =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap g (f x))
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)
-- Mathlib.Order.Grade
instWellFoundedGTOfGradeOrderOrderDualNat : ∀ {α : Type u_3} [inst : Preorder α] [GradeOrder ℕᵒᵈ α], WellFoundedGT α
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams.mk.injEq : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier) (text? : Option String)
  (textDocument_1 : Lean.Lsp.TextDocumentIdentifier) (text?_1 : Option String),
  ({ textDocument := textDocument, text? := text? } = { textDocument := textDocument_1, text? := text?_1 }) =
    (textDocument = textDocument_1 ∧ text? = text?_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertIfNew! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    l.Ordered →
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v l).toListModel.Perm
        (Std.Internal.List.insertEntryIfNew k v l.toListModel)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_dblY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblY (⇑f ∘ P) = f (W'.dblY P)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Iso_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L')
  (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R)
  (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L')
  (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L)
  (hββ' :
    CategoryTheory.CategoryStruct.comp R.rightUnitor.hom
        (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R)
            (F.functor.associator F.inverse R).hom)) =
      CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom)
        (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse)
            (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β')))))
  (hβ'β :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom
          (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β)
            (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv
              (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) =
      CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom
        (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom)
          (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))),
  (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).unitIso =
    (CategoryTheory.StructuredArrow.map₂IdIso L (CategoryTheory.CategoryStruct.id L)
          (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv) ⋯ ⋯).symm ≪≫
      CategoryTheory.StructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.id L)
          (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv) F.unitIso G.unitIso
          (CategoryTheory.CategoryStruct.comp α' (G.inverse.map α))
          (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse)
              (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom
                (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft β')
                  (F.functor.associator F.inverse R).inv))))
          ⋯ ⋯ ≪≫
        (CategoryTheory.StructuredArrow.map₂CompMap₂Iso α' β' α β).symm
-- Lean.Parser.Syntax
Lean.Parser.precedenceParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioi_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n),
  ∑ i > a.succ, f i = ∑ i > a, f i.succ
-- Mathlib.Logic.Equiv.Prod
Equiv.sumArrowEquivProdArrow_apply_snd : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α ⊕ β → γ) (b : β),
  ((Equiv.sumArrowEquivProdArrow α β γ) f).2 b = f (Sum.inr b)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.next_eq_self : ∀ {ι : Type u_1} (c : ComplexShape ι) (j : ι), ¬c.Rel j (c.next j) → c.next j = j
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- A morphism between algebras of endofunctor `F`  -/
CategoryTheory.Endofunctor.Algebra.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      CategoryTheory.Endofunctor.Algebra F → CategoryTheory.Endofunctor.Algebra F → Type v
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The type of morphisms in `AddMonCat`.  -/
AddMonCat.Hom : AddMonCat → AddMonCat → Type u
-- Init.Data.Order.Factories
/-- If an `LE α` instance is antisymmetric, transitive and total, then it represents a linear order.
 -/
Std.IsLinearOrder.of_le : ∀ {α : Type u} [inst : LE α],
  autoParam (Std.Antisymm fun x1 x2 => x1 ≤ x2) Std.IsLinearOrder.of_le._auto_1 →
    ∀
      (le_trans :
        autoParam (Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2)
          Std.IsLinearOrder.of_le._auto_3),
      autoParam (Std.Total fun x1 x2 => x1 ≤ x2) Std.IsLinearOrder.of_le._auto_5 → Std.IsLinearOrder α
-- Mathlib.Data.List.AList
AList.insert_of_notMem : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s : AList β} (h : a ∉ s),
  AList.insert a b s = { entries := ⟨a, b⟩ :: s.entries, nodupKeys := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The functorial (distinguished) triangle
`(t.truncLT a).obj X ⟶ (t.truncLT b).obj X ⟶ (t.truncGELT a b).obj X ⟶ ...`
when `a ≤ b`.  -/
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                (a b : ℤ) → a ≤ b → CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Init.Data.UInt.Lemmas
instCommutativeUInt64HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Init.Data.List.Basic
List.modifyHead.eq_2 : ∀ {α : Type u} (f : α → α) (a : α) (as : List α), List.modifyHead f (a :: as) = f a :: as
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
mem_nonUnitalSubalgebraOfNonUnitalSubring : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {x : R} {S : NonUnitalSubring R},
  x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {toModuleCat : ModuleCat R} {instCoalgebra : Coalgebra R ↑toModuleCat}
  {toModuleCat_1 : ModuleCat R} {instCoalgebra_1 : Coalgebra R ↑toModuleCat_1},
  { toModuleCat := toModuleCat, instCoalgebra := instCoalgebra } =
      { toModuleCat := toModuleCat_1, instCoalgebra := instCoalgebra_1 } →
    toModuleCat = toModuleCat_1 ∧ instCoalgebra ≍ instCoalgebra_1
-- Mathlib.Data.Set.NAry
Set.image2_image_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : γ → β → δ) (g : α → γ),
  Set.image2 f (g '' s) t = Set.image2 (fun a b => f (g a) b) s t
-- Std.Sat.AIG.LawfulOperator
/-- The prefix and the other array must agree on all elements up until the bound of the prefix
 -/
Std.Sat.AIG.IsPrefix.idx_eq : ∀ {α : Type} {decls1 decls2 : Array (Std.Sat.AIG.Decl α)} (self : Std.Sat.AIG.IsPrefix decls1 decls2) (idx : ℕ)
  (h : idx < decls1.size), decls2[idx] = decls1[idx]
-- Init.Data.List.Lemmas
List.filterMap_filter : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → Option β} {l : List α},
  List.filterMap f (List.filter p l) = List.filterMap (fun x => if p x = true then f x else none) l
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_iSup : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} {x : α} {s : ι → TopologicalSpace.Opens α},
  x ∈ iSup s ↔ ∃ i, x ∈ s i
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.id_apply' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u}
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S], PolynomialLaw.id.toFun' S = id
-- Std.Time.Format.Modifier
Std.Time.Modifier.L.sizeOf_spec : ∀ (presentation : Std.Time.Number ⊕ Std.Time.Text), sizeOf (Std.Time.Modifier.L presentation) = 1 + sizeOf presentation
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMapRingHom_apply : ∀ {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₁] (self : M₁ →L[R₁] M₁),
  ContinuousLinearMap.toLinearMapRingHom self = ↑self
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- **Alias** of the forward direction of `ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection`. -/
ContinuousLinearMap.IsStarProjection.isSymmetricProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsStarProjection T → (↑T).IsSymmetricProjection
-- Mathlib.Topology.Order.Lattice
/-- The infimum is continuous  -/
ContinuousInf.continuous_inf : ∀ {L : Type u_1} {inst : TopologicalSpace L} {inst_1 : Min L} [self : ContinuousInf L], Continuous fun p => p.1 ⊓ p.2
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instLinearOrder : {α : Type u_1} → [inst : AddMonoid α] → [LinearOrder α] → LinearOrder (AddUnits α)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_top : ∀ {M : Type u_1} [inst : AddMonoid M], ⊤.addUnits = ⊤
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropy_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X), Antitone fun u => Dynamics.coverEntropy T F
-- Mathlib.Order.Hom.Bounded
/-- Reinterpret a `BoundedOrderHom` as a `TopHom`.  -/
BoundedOrderHom.toTopHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedOrderHom α β → TopHom α β
-- Mathlib.Condensed.Solid
/-- The free condensed `R`-module on a finite set.  -/
Condensed.finFree : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Functor FintypeCat (CondensedMod R)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.invFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  [inst_2 : Nonempty α] (hf : MeasurableEmbedding f) (x : β),
  hf.invFun x = if hx : x ∈ Set.range f then hf.equivRange.symm ⟨x, hx⟩ else ⋯.some
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subLeft_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [IsTopologicalAddGroup H] [inst_3 : PartialOrder H]
  [IsOrderedAddMonoid H] {c a : H},
  Filter.map (fun x => c - x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c - a) (Set.Iio (c - a))
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
NormedRing.toRingNorm_toFun : ∀ (R : Type u_2) [inst : NormedRing R] (a : R), (NormedRing.toRingNorm R).toFun a = ‖a‖
-- Aesop.Builder.Cases
Aesop.CasesPattern.check : Lean.Name → Aesop.CasesPattern → Lean.MetaM Unit
-- Mathlib.Tactic.Simproc.Divisors
_private.Mathlib.Tactic.Simproc.Divisors.0.Nat.properDivisors_ofNat.unsafe_4 : ℕ → Lean.TransformStep
-- Mathlib.Order.Hom.BoundedLattice
/-- A `BoundedLatticeHomClass` morphism preserves the top element.  -/
BoundedLatticeHomClass.map_top : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β] (f : F), f ⊤ = ⊤
-- Lean.Elab.InfoTree.Main
Lean.Elab.TacticInfo.format : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → IO Std.Format
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_sub_natCast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  [inst_4 : Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ), ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.root_gcd_iff_root_left_right : ∀ {R : Type u} {k : Type y} [inst : Field R] [inst_1 : CommSemiring k] [inst_2 : DecidableEq R] {ϕ : R →+* k}
  {f g : Polynomial R} {α : k},
  Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 ↔ Polynomial.eval₂ ϕ α f = 0 ∧ Polynomial.eval₂ ϕ α g = 0
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If `Φ : LocalizerMorphism W₁ W₂`, the typeclass `Φ.IsInduced`
says that `W₂.inverseImage Φ.functor = W₁`.  -/
CategoryTheory.LocalizerMorphism.IsInduced : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.PComp.mk : Mathlib.Tactic.Linarith.Comp →
  Mathlib.Tactic.Linarith.CompSource →
    Std.TreeSet ℕ compare →
      Std.TreeSet ℕ compare → Std.TreeSet ℕ compare → Std.TreeSet ℕ compare → Mathlib.Tactic.Linarith.PComp
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_zero_le_veblenWith_zero : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}},
  Order.IsNormal f → 0 < f 0 → (Ordinal.veblenWith f o₁ 0 ≤ Ordinal.veblenWith f o₂ 0 ↔ o₁ ≤ o₂)
-- Mathlib.GroupTheory.Focal
/-- The restriction of the transfer map to `H` acts like the power map `x ↦ x^n` mod `H*`,
where `n = [G:H]`.
 -/
Subgroup.transferFocal_eq_pow : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.FiniteIndex] (x : ↥H), H.transferFocal ↑x = ↑x ^ H.index
-- Init.Data.String.Defs
String.Slice.Pos.mk.sizeOf_spec : ∀ {s : String.Slice} (offset : String.Pos.Raw) (isValidForSlice : String.Pos.Raw.IsValidForSlice s offset),
  sizeOf { offset := offset, isValidForSlice := isValidForSlice } = 1 + sizeOf offset + sizeOf isValidForSlice
-- Mathlib.Order.RelIso.Basic
RelEmbedding.antisymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [Std.Antisymm s], Std.Antisymm r